1  /-
  2  Copyright (c) 2017 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Mario Carneiro
  5  -/
  6  import number_theory.pell data.pfun
src         └────────────────┘ └───────┘
  7  
  8  universe u
  9  
 10  open nat function
 11  
 12  namespace int
 13  
 14  lemma eq_nat_abs_iff_mul (x n) : nat_abs x = n ↔ (x - n) * (x + n) = 0 :=
id                                    └─────┘                
src                                   └─────┘                      
typ                                   └─────┘                
 15  begin
 16    refine iff.trans _ mul_eq_zero.symm,
src    └─────┘         └─┘
typ    └─────┘         └─┘
doc    └─────┘         └─┘
txt    └─────┘         └─┘
par    └─────┘         └─┘
pid                   └─┘
 17    refine iff.trans _ (or_congr sub_eq_zero add_eq_zero_iff_eq_neg).symm,
src    └─────┘         └─┘                                          └────┘
typ    └─────┘         └─┘                                          └────┘
doc    └─────┘         └─┘                                          └────┘
txt    └─────┘         └─┘                                          └────┘
par    └─────┘         └─┘                                          └────┘
pid                   └─┘                                          └───┘
 18    exact ⟨λe, by rw ← e; apply nat_abs_eq,
id                                └────────┘
src    └────┘  └─┘  └───┘ └┘└────┘└────────┘└─
typ    └────┘  └─┘  └───┘└──────┘└────────┘└─
doc    └────┘  └─┘  └───┘ └┘└────┘          └─
txt    └────┘  └─┘  └───┘ └┘└────┘          └─
par    └────┘  └─┘  └───┘ └──────┘          └─
pid           └─┘  └────┘ └──────┘          └─
st                    └─────────────────────┘└─
 19      λo, by cases o; subst x; simp [nat_abs_of_nat]⟩
id                                    └────────────┘
src  ───┘ └─┘  └────┘ └┘└────┘ └┘└────┘└────────────┘└┘
typ  ───┘ └─┘  └────┘└──────┘└┘└────┘└────────────┘└┘
doc  ───┘ └─┘  └────┘ └┘└────┘ └┘└────┘              └┘
txt  ───┘ └─┘  └────┘ └┘└────┘ └┘└────┘              └┘
par  ───┘ └─┘  └────┘ └──────┘ └┘└────┘              └┘
pid  ───┘ └─┘  └─────┘ └──────┘ └──────┘              └┘
st   ─────────┘└──────────────────────────────────────┘└┘
 20  end
st   └─┘
 21  
 22  end int
 23  
 24  /-- An alternate definition of `fin n` defined as an inductive type
 25    instead of a subtype of `nat`. This is useful for its induction
 26    principle and different definitional equalities. -/
 27  inductive fin2 : ℕ → Type
id                    
src                   
typ                   
 28  | fz {n} : fin2 (succ n)
id                   └──┘ 
src                   └──┘
typ                  └──┘ 
 29  | fs {n} : fin2 n → fin2 (succ n)
id             └──┘          └──┘ 
src                            └──┘
typ            └──┘          └──┘ 
 30  
 31  namespace fin2
 32  
 33  @[elab_as_eliminator]
doc    └────────────────┘
 34  protected def cases' {n} {C : fin2 (succ n) → Sort u} (H1 : C fz) (H2 : Π n, C (fs n)) :
id                                 └──┘  └──┘                    └┘              └┘ 
src                                └──┘  └──┘                      └┘                └┘
typ                                └──┘  └──┘                    └┘              └┘ 
doc                                └──┘
 35    Π (i : fin2 (succ n)), C i
id           └──┘  └──┘      
src           └──┘  └──┘
typ          └──┘  └──┘      
doc           └──┘
 36  | fz     := H1
id     └┘        └┘
src    └┘
typ    └┘        └┘
 37  | (fs n) := H2 n
id      └┘      └┘
src     └┘
typ     └┘      └┘
 38  
 39  def elim0 {C : fin2 0 → Sort u} : Π (i : fin2 0), C i.
id                  └──┘                     └──┘      └┘
src                 └──┘                      └──┘
typ                 └──┘                     └──┘      └┘
doc                 └──┘                      └──┘
 40  
 41  /-- convert a `fin2` into a `nat` -/
 42  def to_nat : Π {n}, fin2 n → ℕ
id                     └──┘    
src                      └──┘     
typ                    └──┘    
doc                      └──┘
 43  | ._ (@fz n)   := 0
id          └┘
src         └┘
typ         └┘
 44  | ._ (@fs n i) := succ (to_nat i)
id          └┘        └──┘  └────┘
src         └┘         └──┘
typ         └┘        └──┘  └────┘
 45  
 46  /-- convert a `nat` into a `fin2` if it is in range -/
 47  def opt_of_nat : Π {n} (k : ℕ), option (fin2 n)
id                                └────┘  └──┘ 
src                                 └────┘  └──┘
typ                               └────┘  └──┘ 
doc                                          └──┘
 48  | 0 _ := none
id            └──┘
src           └──┘
typ           └──┘
 49  | (succ n) 0 := some fz
id      └──┘         └──┘ └┘
src     └──┘         └──┘ └┘
typ     └──┘         └──┘ └┘
 50  | (succ n) (succ k) := fs <$> @opt_of_nat n k
id              └──┘      └┘ └─┘  └────────┘
src              └──┘       └┘ └─┘
typ             └──┘      └┘ └─┘  └────────┘
 51  
 52  /-- `i + k : fin2 (n + k)` when `i : fin2 n` and `k : ℕ` -/
 53  def add {n} (i : fin2 n) : Π k, fin2 (n + k)
id                    └──┘         └──┘    
src                   └──┘           └──┘    
typ                   └──┘         └──┘    
doc                   └──┘           └──┘
 54  | 0        := i
id                 
typ                
 55  | (succ k) := fs (add k)
id      └──┘      └┘  └─┘
src     └──┘       └┘
typ     └──┘      └┘  └─┘
 56  
 57  /-- `left k` is the embedding `fin2 n → fin2 (k + n)` -/
 58  def left (k) : Π {n}, fin2 n → fin2 (k + n)
id                       └──┘    └──┘    
src                        └──┘     └──┘    
typ                      └──┘    └──┘    
doc                        └──┘     └──┘
 59  | ._ (@fz n)   := fz
id          └┘         └┘
src         └┘         └┘
typ         └┘         └┘
 60  | ._ (@fs n i) := fs (left i)
id          └┘        └┘  └──┘
src         └┘         └┘
typ         └┘        └┘  └──┘
 61  
 62  /-- `insert_perm a` is a permutation of `fin2 n` with the following properties:
 63    * `insert_perm a i = i+1` if `i < a`
 64    * `insert_perm a a = 0`
 65    * `insert_perm a i = i` if `i > a` -/
 66  def insert_perm : Π {n}, fin2 n → fin2 n → fin2 n
id                          └──┘    └──┘    └──┘ 
src                           └──┘     └──┘     └──┘
typ                         └──┘    └──┘    └──┘ 
doc                           └──┘     └──┘     └──┘
 67  | ._ (@fz n)          (@fz ._)   := fz
id                           └┘          └┘
src                          └┘          └┘
typ                          └┘          └┘
 68  | ._ (@fz n)          (@fs ._ j) := fs j
id          └┘               └┘         └┘
src         └┘               └┘          └┘
typ         └┘               └┘         └┘
 69  | ._ (@fs (succ n) i) (@fz ._)   := fs fz
id          └┘  └──┘         └┘          └┘ └┘
src         └┘  └──┘         └┘          └┘ └┘
typ         └┘  └──┘         └┘          └┘ └┘
 70  | ._ (@fs (succ n) i) (@fs ._ j) := match insert_perm i j with fz := fz | fs k := fs (fs k) end
id              └──┘        └┘               └─────────┘          └┘    └┘   └┘     └┘  └┘
src             └──┘         └┘                                     └┘    └┘   └┘      └┘  └┘
typ             └──┘        └┘               └─────────┘          └┘    └┘   └┘     └┘  └┘
 71  
 72  /-- `remap_left f k : fin2 (m + k) → fin2 (n + k)` applies the function
 73    `f : fin2 m → fin2 n` to inputs less than `m`, and leaves the right part
 74    on the right (that is, `remap_left f k (m + i) = n + i`). -/
 75  def remap_left {m n} (f : fin2 m → fin2 n) : Π k, fin2 (m + k) → fin2 (n + k)
id                             └──┘    └──┘         └──┘        └──┘    
src                            └──┘     └──┘           └──┘          └──┘    
typ                            └──┘    └──┘         └──┘        └──┘    
doc                            └──┘     └──┘           └──┘           └──┘
 76  | 0        i          := f i
id                           
typ                          
 77  | (succ k) (@fz ._)   := fz
id      └──┘      └┘          └┘
src     └──┘      └┘          └┘
typ     └──┘      └┘          └┘
 78  | (succ k) (@fs ._ i) := fs (remap_left _ i)
id      └──┘      └┘         └┘  └────────┘
src     └──┘      └┘          └┘
typ     └──┘      └┘         └┘  └────────┘
 79  
 80  /-- This is a simple type class inference prover for proof obligations
 81    of the form `m < n` where `m n : ℕ`. -/
 82  class is_lt (m n : ℕ) := (h : m < n)
id                                  
src                                 
typ                                 
 83  instance is_lt.zero (n) : is_lt 0 (succ n) := ⟨succ_pos _⟩
id                             └───┘    └──┘       └──────┘
src                            └───┘    └──┘        └──────┘
typ                            └───┘    └──┘       └──────┘
doc                            └───┘
 84  instance is_lt.succ (m n) [l : is_lt m n] : is_lt (succ m) (succ n) := ⟨succ_lt_succ l.h⟩
id                                  └───┘      └───┘  └──┘    └──┘       └──────────┘ └┘
src                                 └───┘        └───┘  └──┘     └──┘        └──────────┘  └┘
typ                                 └───┘      └───┘  └──┘    └──┘       └──────────┘ └┘
doc                                 └───┘        └───┘
 85  
 86  /-- Use type class inference to infer the boundedness proof, so that we
 87    can directly convert a `nat` into a `fin2 n`. This supports
 88    notation like `&1 : fin 3`. -/
 89  def of_nat' : Π {n} m [is_lt m n], fin2 n
id                       └───┘     └──┘ 
src                         └───┘       └──┘
typ                      └───┘     └──┘ 
doc                         └───┘       └──┘
 90  | 0        m        ⟨h⟩ := absurd h (not_lt_zero _)
id                             └────┘    └─────────┘
src                             └────┘    └─────────┘
typ                            └────┘    └─────────┘
 91  | (succ n) 0        ⟨h⟩ := fz
id      └──┘                    └┘
src     └──┘                    └┘
typ     └──┘                    └┘
 92  | (succ n) (succ m) ⟨h⟩ := fs (@of_nat' n m ⟨lt_of_succ_lt_succ h⟩)
id              └──┘         └┘   └─────┘      └────────────────┘
src              └──┘           └┘                └────────────────┘
typ             └──┘         └┘   └─────┘      └────────────────┘
 93  
 94  local prefix `&`:max := of_nat'
id                    └─┘    └─────┘
src                   └─┘    └─────┘
typ                   └─┘    └─────┘
doc                          └─────┘
 95  
 96  end fin2
 97  
 98  open fin2
 99  
100  /-- Alternate definition of `vector` based on `fin2`. -/
101  def vector3 (α : Type u) (n : ℕ) : Type u := fin2 n → α
id                                               └──┘    
src                                              └──┘
typ                                              └──┘    
doc                                               └──┘
102  
103  namespace vector3
104  
105  /-- The empty vector -/
106  @[pattern] def nil {α} : vector3 α 0.
id                            └─────┘ 
src                           └─────┘
typ                           └─────┘ 
doc    └─────┘                └─────┘
107  
108  /-- The vector cons operation -/
109  @[pattern] def cons {α} {n} (a : α) (v : vector3 α n) : vector3 α (succ n) :=
id                                           └─────┘      └─────┘   └──┘ 
src                                           └─────┘        └─────┘    └──┘
typ                                          └─────┘      └─────┘   └──┘ 
doc    └─────┘                                └─────┘        └─────┘
110  λi, by {refine i.cases' _ _, exact a, exact v}
id                 └──────┘                    
src          └─────┘└──────┘└──┘  └────┘   └────┘
typ         └─────┘└──────┘└──┘  └────┘  └────┘
doc          └─────┘        └──┘  └────┘   └────┘
txt          └─────┘        └──┘  └────┘   └────┘
par          └─────┘        └──┘  └────┘   └────┘
pid                        └──┘               
st         └───────────────────┘└───────┘└───────┘└┘
111  
112  /- We do not want to make the following notation global, because then these expressions will be
113  overloaded, and only the expected type will be able to disambiguate the meaning. Worse: Lean will
114  try to insert a coercion from `vector3 α _` to `list α`, if a list is expected. -/
115  localized "notation `[` l:(foldr `, ` (h t, vector3.cons h t) nil `]`) := l" in vector3
116  notation a :: b := cons a b
id                      └──┘
src                     └──┘
typ                     └──┘
doc                     └──┘
117  
118  @[simp] theorem cons_fz {α} {n} (a : α) (v : vector3 α n) : (a :: v) fz = a := rfl
id                                               └─────┘        └┘   └┘      └─┘
src                                               └─────┘           └┘    └┘       └─┘
typ                                              └─────┘        └┘   └┘      └─┘
doc    └──┘                                       └─────┘           └┘
119  @[simp] theorem cons_fs {α} {n} (a : α) (v : vector3 α n) (i) : (a :: v) (fs i) = v i := rfl
id                                               └─────┘            └┘    └┘         └─┘
src                                               └─────┘               └┘     └┘            └─┘
typ                                              └─────┘            └┘    └┘         └─┘
doc    └──┘                                       └─────┘               └┘
120  
121  /-- Get the `i`th element of a vector -/
122  @[reducible] def nth {α} {n} (i : fin2 n) (v : vector3 α n) : α := v i
id                                     └──┘        └─────┘           
src                                    └──┘         └─────┘
typ                                    └──┘        └─────┘           
doc    └───────┘                       └──┘         └─────┘
123  
124  /-- Construct a vector from a function on `fin2`. -/
125  @[reducible] def of_fn {α} {n} (f : fin2 n → α) : vector3 α n := f
id                                       └──┘        └─────┘      
src                                      └──┘          └─────┘
typ                                      └──┘        └─────┘      
doc    └───────┘                         └──┘          └─────┘
126  
127  /-- Get the head of a nonempty vector. -/
128  def head {α} {n} (v : vector3 α (succ n)) : α := v fz
id                         └─────┘   └──┘           └┘
src                        └─────┘    └──┘              └┘
typ                        └─────┘   └──┘           └┘
doc                        └─────┘
129  
130  /-- Get the tail of a nonempty vector. -/
131  def tail {α} {n} (v : vector3 α (succ n)) : vector3 α n := λi, v (fs i)
id                         └─────┘   └──┘      └─────┘           └┘ 
src                        └─────┘    └──┘       └─────┘               └┘
typ                        └─────┘   └──┘      └─────┘           └┘ 
doc                        └─────┘               └─────┘
132  
133  theorem eq_nil {α} (v : vector3 α 0) : v = [] :=
id                           └─────┘         └┘
src                          └─────┘           └┘
typ                          └─────┘         └┘
doc                          └─────┘            └┘
134  funext $ λi, match i with end
id   └────┘            
src  └────┘
typ  └────┘            
135  
136  theorem cons_head_tail {α} {n} (v : vector3 α (succ n)) : head v :: tail v = v :=
id                                       └─────┘   └──┘      └──┘  └┘ └──┘   
src                                      └─────┘    └──┘       └──┘   └┘ └──┘   
typ                                      └─────┘   └──┘      └──┘  └┘ └──┘   
doc                                      └─────┘               └──┘   └┘ └──┘
137  funext $ λi, fin2.cases' rfl (λ_, rfl) i
id   └────┘      └─────────┘ └─┘     └─┘  
src  └────┘       └─────────┘ └─┘      └─┘
typ  └────┘      └─────────┘ └─┘     └─┘  
138  
139  def nil_elim {α} {C : vector3 α 0 → Sort u} (H : C []) (v : vector3 α 0) : C v :=
id                         └─────┘                    └┘       └─────┘        
src                        └─────┘                      └┘       └─────┘
typ                        └─────┘                    └┘       └─────┘        
doc                        └─────┘                      └┘       └─────┘
140  by rw eq_nil v; apply H
id         └────┘ 
src     └─┘└────┘   └────┘ 
typ     └─┘└────┘  └────┘ 
doc     └─┘         └────┘ 
txt     └─┘         └────┘ 
par     └─┘         └────┘ 
pid                      
st     └─────────────────────
141  
src  
typ  
doc  
txt  
par  
pid  
st   
142  def cons_elim {α n} {C : vector3 α (succ n) → Sort u} (H : Π (a : α) (t : vector3 α n), C (a :: t))
id                            └─────┘   └──┘                                └─────┘        └┘ 
src                           └─────┘    └──┘                                  └─────┘            └┘
typ                           └─────┘   └──┘                                └─────┘        └┘ 
doc                           └─────┘                                          └─────┘            └┘
143    (v : vector3 α (succ n)) : C v :=
id          └─────┘   └──┘       
src         └─────┘    └──┘
typ         └─────┘   └──┘       
doc         └─────┘
144  by rw ← (cons_head_tail v); apply H
id            └────────────┘ 
src     └───┘ └────────────┘   └────┘ 
typ     └───┘ └────────────┘  └────┘ 
doc     └───┘                  └────┘ 
txt     └───┘                  └────┘ 
par     └───┘                  └────┘ 
pid       └─┘                        
st     └─────────────────────────────────
145  
src  
typ  
doc  
txt  
par  
pid  
st   
146  @[simp] theorem cons_elim_cons {α n C H a t} : @cons_elim α n C H (a :: t) = H a t := rfl
id                                                   └───────┘       └┘          └─┘
src                                                  └───────┘            └┘              └─┘
typ                                                  └───────┘       └┘          └─┘
doc    └──┘                                                               └┘
147  
148  @[elab_as_eliminator]
doc    └────────────────┘
149  protected def rec_on {α} {C : Π {n}, vector3 α n → Sort u} {n} (v : vector3 α n)
id                                       └─────┘                      └─────┘  
src                                       └─────┘                        └─────┘
typ                                      └─────┘                      └─────┘  
doc                                       └─────┘                        └─────┘
150    (H0 : C [])
id            └┘
src            └┘
typ           └┘
doc            └┘
151    (Hs : Π {n} (a) (w : vector3 α n), C w → C (a :: w)) : C v :=
id                        └─────┘            └┘       
src                         └─────┘                  └┘
typ                       └─────┘            └┘       
doc                         └─────┘                  └┘
152  nat.rec_on n
id   └────────┘ 
src  └────────┘
typ  └────────┘ 
153    (λv, v.nil_elim H0)
id         └───────┘ └┘
src          └───────┘
typ        └───────┘ └┘
154    (λn IH v, v.cons_elim (λa t, Hs _ _ (IH _))) v
id        └┘   └────────┘      └┘      └┘      
src               └────────┘
typ       └┘   └────────┘      └┘      └┘      
155  
156  @[simp] theorem rec_on_nil {α C H0 Hs} : @vector3.rec_on α @C 0 [] H0 @Hs = H0 :=
id                                             └────────────┘      └┘ └┘  └┘  └┘
src                                            └────────────┘        └┘        
typ                                            └────────────┘      └┘ └┘  └┘  └┘
doc    └──┘                                                          └┘
157  rfl
id   └─┘
src  └─┘
typ  └─┘
158  
159  @[simp] theorem rec_on_cons {α C H0 Hs n a v} :
doc    └──┘
160    @vector3.rec_on α @C (succ n) (a :: v) H0 @Hs = Hs a v (@vector3.rec_on α @C n v H0 @Hs) :=
id      └────────────┘     └──┘     └┘   └┘  └┘  └┘     └────────────┘      └┘  └┘
src     └────────────┘       └──┘       └┘                     └────────────┘
typ     └────────────┘     └──┘     └┘   └┘  └┘  └┘     └────────────┘      └┘  └┘
doc                                     └┘
161  rfl
id   └─┘
src  └─┘
typ  └─┘
162  
163  /-- Append two vectors -/
164  def append {α} {m} (v : vector3 α m) {n} (w : vector3 α n) : vector3 α (n+m) :=
id                           └─────┘             └─────┘      └─────┘   
src                          └─────┘               └─────┘        └─────┘     
typ                          └─────┘             └─────┘      └─────┘   
doc                          └─────┘               └─────┘        └─────┘
165  nat.rec_on m (λ_, w) (λm IH v, v.cons_elim $ λa t, @fin2.cases' (n+m) (λ_, α) a (IH t)) v
id   └────────┘           └┘   └────────┘        └─────────┘            └┘    
src  └────────┘                      └────────┘          └─────────┘   
typ  └────────┘           └┘   └────────┘        └─────────┘            └┘    
166  
167  local infix ` +-+ `:65 := vector3.append
id                             └────────────┘
src                            └────────────┘
typ                            └────────────┘
doc                            └────────────┘
168  
169  @[simp] theorem append_nil {α} {n} (w : vector3 α n) : [] +-+ w = w := rfl
id                                           └─────┘      └┘ └─┘       └─┘
src                                          └─────┘        └┘ └─┘         └─┘
typ                                          └─────┘      └┘ └─┘       └─┘
doc    └──┘                                  └─────┘        └┘ └─┘
170  
171  @[simp] theorem append_cons {α} (a : α) {m} (v : vector3 α m) {n} (w : vector3 α n) :
id                                                   └─────┘             └─────┘  
src                                                   └─────┘               └─────┘
typ                                                  └─────┘             └─────┘  
doc    └──┘                                           └─────┘               └─────┘
172    (a::v) +-+ w = a :: (v +-+ w) := rfl
id      └┘  └─┘    └┘   └─┘      └─┘
src      └┘   └─┘      └┘    └─┘       └─┘
typ     └┘  └─┘    └┘   └─┘      └─┘
doc      └┘   └─┘       └┘    └─┘
173  
174  @[simp] theorem append_left {α} : ∀ {m} (i : fin2 m) (v : vector3 α m) {n} (w : vector3 α n),
id                                              └──┘        └─────┘            └─────┘  
src                                               └──┘         └─────┘               └─────┘
typ                                             └──┘        └─────┘            └─────┘  
doc    └──┘                                       └──┘         └─────┘               └─────┘
175    (v +-+ w) (left n i) = v i
id       └─┘    └──┘      
src       └─┘     └──┘      
typ      └─┘    └──┘      
doc       └─┘     └──┘
176  | ._ (@fz m)   v n w := v.cons_elim (λa t, by simp [*, left])
id          └┘               └────────┘                  └──┘
src         └┘                └────────┘           └───────┘└──┘
typ         └┘               └────────┘         └───────┘└──┘
doc                                                └───────┘└──┘
txt                                                └───────┘    
par                                                └───────┘    
pid                                                    └──┘    
st                                                └─────────────┘
177  | ._ (@fs m i) v n w := v.cons_elim (λa t, by simp [*, left])
id          └┘               └────────┘                  └──┘
src         └┘                └────────┘           └───────┘└──┘
typ         └┘               └────────┘         └───────┘└──┘
doc                                                └───────┘└──┘
txt                                                └───────┘    
par                                                └───────┘    
pid                                                    └──┘    
st                                                └─────────────┘
178  
179  @[simp] theorem append_add {α} : ∀ {m} (v : vector3 α m) {n} (w : vector3 α n) (i : fin2 n),
id                                             └─────┘            └─────┘         └──┘ 
src                                              └─────┘               └─────┘           └──┘
typ                                            └─────┘            └─────┘         └──┘ 
doc    └──┘                                      └─────┘               └─────┘           └──┘
180    (v +-+ w) (add i m) = w i
id       └─┘    └─┘      
src       └─┘     └─┘      
typ      └─┘    └─┘      
doc       └─┘     └─┘
181  | 0        v n w i := rfl
id                         └─┘
src                        └─┘
typ                        └─┘
182  | (succ m) v n w i := v.cons_elim (λa t, by simp [*, add])
id      └──┘               └────────┘                  └─┘
src     └──┘                └────────┘           └───────┘└─┘
typ     └──┘               └────────┘         └───────┘└─┘
doc                                              └───────┘└─┘
txt                                              └───────┘   
par                                              └───────┘   
pid                                                  └──┘   
st                                              └────────────┘
183  
184  /-- Insert `a` into `v` at index `i`. -/
185  def insert {α} (a : α) {n} (v : vector3 α n) (i : fin2 (succ n)) : vector3 α (succ n) :=
id                                  └─────┘         └──┘  └──┘      └─────┘   └──┘ 
src                                  └─────┘           └──┘  └──┘       └─────┘    └──┘
typ                                 └─────┘         └──┘  └──┘      └─────┘   └──┘ 
doc                                  └─────┘           └──┘             └─────┘
186  λj, (a :: v) (insert_perm i j)
id        └┘    └─────────┘  
src         └┘     └─────────┘
typ       └┘    └─────────┘  
doc         └┘     └─────────┘
187  
188  @[simp] theorem insert_fz {α} (a : α) {n} (v : vector3 α n) : insert a v fz = a :: v :=
id                                                 └─────┘      └────┘   └┘   └┘ 
src                                                 └─────┘        └────┘     └┘    └┘
typ                                                └─────┘      └────┘   └┘   └┘ 
doc    └──┘                                         └─────┘        └────┘            └┘
189  by refine funext (λj, j.cases' _ _); intros; refl
id             └────┘       └─────┘
src     └─────┘└────┘  └─┘ └─────┘└───┘  └────┘  └────
typ     └─────┘└────┘  └─┘ └─────┘└───┘  └────┘  └────
doc     └─────┘        └─┘        └───┘  └────┘  └────
txt     └─────┘        └─┘        └───┘  └────┘  └────
par     └─────┘        └─┘        └───┘  └────┘  └────
pid                   └─┘        └───┘              
st     └───────────────────────────────────────────────
190  
src  
typ  
doc  
txt  
par  
pid  
st   
191  @[simp] theorem insert_fs {α} (a : α) {n} (b : α) (v : vector3 α n) (i : fin2 (succ n)) :
id                                                        └─────┘         └──┘  └──┘ 
src                                                         └─────┘           └──┘  └──┘
typ                                                       └─────┘         └──┘  └──┘ 
doc    └──┘                                                 └─────┘           └──┘
192    insert a (b :: v) (fs i) = b :: insert a v i :=
id     └────┘    └┘    └┘     └┘ └────┘   
src    └────┘      └┘     └┘       └┘ └────┘
typ    └────┘    └┘    └┘     └┘ └────┘   
doc    └────┘      └┘               └┘ └────┘
193  funext $ λj, by {
id   └────┘    
src  └────┘
typ  └────┘    
st                  └──
194    refine j.cases' _ (λj, _); simp [insert, insert_perm],
id            └──────┘                  └────┘  └─────────┘
src    └─────┘└──────┘└─┘  └───┘  └────┘└────┘└┘└─────────┘
typ    └─────┘└──────┘└─┘  └───┘  └────┘└────┘└┘└─────────┘
doc    └─────┘        └─┘  └───┘  └────┘└────┘└┘└─────────┘
txt    └─────┘        └─┘  └───┘  └────┘      └┘           
par    └─────┘        └─┘  └───┘  └────┘      └┘           
pid                  └─┘  └───┘            └┘           
st   ──────────────────────────────────────────────────────┘└─
195    refine fin2.cases' _ _ (insert_perm i j); simp [insert_perm] }
id            └─────────┘      └─────────┘           └─────────┘
src    └─────┘└─────────┘└───┘ └─────────┘    └────┘└─────────┘└┘
typ    └─────┘└─────────┘└───┘ └─────────┘  └────┘└─────────┘└┘
doc    └─────┘           └───┘ └─────────┘    └────┘└─────────┘└┘
txt    └─────┘           └───┘                └────┘           └┘
par    └─────┘           └───┘                └────┘           └┘
pid                     └───┘                               
st   ──────────────────────────────────────────────────────────────┘└┘
196  
197  theorem append_insert {α} (a : α) {k} (t : vector3 α k) {n} (v : vector3 α n) (i : fin2 (succ n)) (e : succ n + k = succ (n + k)) :
id                                             └─────┘             └─────┘         └──┘  └──┘         └──┘     └──┘    
src                                             └─────┘               └─────┘           └──┘  └──┘          └──┘       └──┘    
typ                                            └─────┘             └─────┘         └──┘  └──┘         └──┘     └──┘    
doc                                             └─────┘               └─────┘           └──┘
198    insert a (t +-+ v) (eq.rec_on e (i.add k)) = eq.rec_on e (t +-+ insert a v i) :=
id     └────┘    └─┘    └───────┘   └──┘     └───────┘    └─┘ └────┘   
src    └────┘      └─┘     └───────┘     └──┘      └───────┘      └─┘ └────┘
typ    └────┘    └─┘    └───────┘   └──┘     └───────┘    └─┘ └────┘   
doc    └────┘      └─┘                   └──┘                      └─┘ └────┘
199  begin
st   └─────
200    refine vector3.rec_on t (λe, _) (λk b t IH e, _) e, refl,
id            └────────────┘                           
src    └─────┘└────────────┘   └────┘  └─────────────┘   └──┘
typ    └─────┘└────────────┘  └────┘  └─────────────┘  └──┘
doc    └─────┘                 └────┘  └─────────────┘   └──┘
txt    └─────┘                 └────┘  └─────────────┘   └──┘
par    └─────┘                 └────┘  └─────────────┘   └──┘
pid                           └────┘  └─────────────┘
st   ───────────────────────────────────────────────────┘└────┘└─
201    have e' := succ_add n k,
id                └──────┘  
src    └─────────┘└──────┘ 
typ    └─────────┘└──────┘
doc    └─────────┘         
txt    └─────────┘         
par    └─────────┘         
pid    └─────┘└─┘         
st   ────────────────────────┘└─
202    change insert a (b :: (t +-+ v)) (eq.rec_on (congr_arg succ e') (fs (add i k)))
id                        └┘    └─┘                                     └┘  └─┘   
src    └─────┘         └┘  └─┘ └─┘                          └┘ └┘ └─┘  └───
typ    └─────┘         └┘  └─┘ └─┘                          └┘ └┘ └─┘ └───
doc    └─────┘         └┘  └─┘ └─┘                          └┘    └─┘  └───
txt    └─────┘                 └─┘                          └┘         └───
par    └─────┘                 └─┘                          └┘         └───
pid                           └─┘                          └┘         └───
st   ──────────────────────────────────────────────────────────────────────────────────
203      = eq.rec_on (congr_arg succ e') (b :: (t +-+ insert a v i)),
id        └───────┘  └───────┘ └──┘ └┘             └────┘   
src  ───┘└───────┘ └───────┘└──┘  └┘         └────┘   └┘
typ  ───┘└───────┘ └───────┘└──┘└┘└┘       └────┘└┘
doc  ───┘                          └┘         └────┘   └┘
txt  ───┘                          └┘                  └┘
par  ───┘                          └┘                  └┘
pid  ───┘                          └┘                  └┘
st   ──────────────────────────────────────────────────────────────┘└─
204    rw ← (eq.drec_on e' rfl : fs (eq.rec_on e' (i.add k) : fin2 (succ (n + k))) = eq.rec_on (congr_arg succ e') (fs (i.add k))),
id           └────────┘ └┘ └─┘                                └──┘                 └───────┘  └───────┘ └──┘      └┘  └───┘ 
src    └───┘ └────────┘  └─┘└─┘                     └──┘└──┘        └──┘ └───────┘ └───────┘└──┘  └┘ └┘ └───┘ └─┘
typ    └───┘ └────────┘└┘└─┘└─┘                     └──┘└──┘       └──┘ └───────┘ └───────┘└──┘  └┘ └┘ └───┘└─┘
doc    └───┘                └─┘                     └──┘└──┘         └──┘                          └┘    └───┘ └─┘
txt    └───┘                └─┘                     └──┘             └──┘                          └┘          └─┘
par    └───┘                └─┘                     └──┘             └──┘                          └┘          └─┘
pid      └─┘                └─┘                     └──┘             └──┘                          └┘          └─┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
205    simp, rw IH, exact eq.drec_on e' rfl
id              └┘        └────────┘ └┘ └─┘
src    └──┘  └─┘    └────┘└────────┘  └─┘
typ    └──┘  └─┘└┘  └────┘└────────┘└┘└─┘
doc    └──┘  └─┘    └────┘               
txt    └──┘  └─┘    └────┘               
par    └──┘  └─┘    └────┘               
pid                                    
st   ─────┘└─────┘└────────────────────────┘
206  end
st   └─┘
207  
208  end vector3
209  
210  section vector3
211  open vector3
212  open_locale vector3
213  
214  /-- "Curried" exists, i.e. ∃ x1 ... xn, f [x1, ..., xn] -/
215  def vector_ex {α} : Π k, (vector3 α k → Prop) → Prop
id                            └─────┘   
src                            └─────┘
typ                           └─────┘   
doc                            └─────┘
216  | 0        f := f []
id                    └┘
src                    └┘
typ                   └┘
doc                    └┘
217  | (succ k) f := ∃x : α, vector_ex k (λv, f (x :: v))
id      └──┘            └───────┘           └┘ 
src     └──┘                                     └┘
typ     └──┘            └───────┘           └┘ 
doc                                                └┘
218  
219  /-- "Curried" forall, i.e. ∀ x1 ... xn, f [x1, ..., xn] -/
220  def vector_all {α} : Π k, (vector3 α k → Prop) → Prop
id                             └─────┘   
src                             └─────┘
typ                            └─────┘   
doc                             └─────┘
221  | 0        f := f []
id                    └┘
src                    └┘
typ                   └┘
doc                    └┘
222  | (succ k) f := ∀x : α, vector_all k (λv, f (x :: v))
id      └──┘              └────────┘           └┘ 
src     └──┘                                        └┘
typ     └──┘              └────────┘           └┘ 
doc                                                 └┘
223  
224  theorem exists_vector_zero {α} (f : vector3 α 0 → Prop) : Exists f ↔ f [] :=
id                                       └─────┘              └────┘    └┘
src                                      └─────┘               └────┘      └┘
typ                                      └─────┘              └────┘    └┘
doc                                      └─────┘                            └┘
225  ⟨λ⟨v, fv⟩, by rw ← (eq_nil v); exact fv, λf0, ⟨[], f0⟩⟩
id                      └────┘          └┘   └┘   └┘  └┘
src                └───┘ └────┘   └────┘          └┘
typ               └───┘ └────┘  └────┘└┘   └┘   └┘  └┘
doc                └───┘          └────┘          └┘
txt                └───┘          └────┘
par                └───┘          └────┘
pid                  └─┘               
st                └────────────────────────┘
226  
227  theorem exists_vector_succ {α n} (f : vector3 α (succ n) → Prop) : Exists f ↔ ∃x v, f (x :: v) :=
id                                         └─────┘   └──┘             └────┘        └┘ 
src                                        └─────┘    └──┘              └────┘             └┘
typ                                        └─────┘   └──┘             └────┘        └┘ 
doc                                        └─────┘                                            └┘
228  ⟨λ⟨v, fv⟩, ⟨_, _, by rw cons_head_tail v; exact fv⟩, λ⟨x, v, fxv⟩, ⟨_, fxv⟩⟩
id                          └────────────┘         └┘          └─┘
src                       └─┘└────────────┘   └────┘
typ                      └─┘└────────────┘  └────┘└┘          └─┘
doc                       └─┘                 └────┘
txt                       └─┘                 └────┘
par                       └─┘                 └────┘
pid                                               
st                       └────────────────────────────┘
229  
230  theorem vector_ex_iff_exists {α} : ∀ {n} (f : vector3 α n → Prop), vector_ex n f ↔ Exists f
id                                               └─────┘           └───────┘    └────┘ 
src                                                └─────┘              └───────┘      └────┘
typ                                              └─────┘           └───────┘    └────┘ 
doc                                                └─────┘              └───────┘
231  | 0        f := (exists_vector_zero f).symm
id                   └────────────────┘   └──┘
src                   └────────────────┘   └──┘
typ                  └────────────────┘   └──┘
232  | (succ n) f := iff.trans (exists_congr (λx, vector_ex_iff_exists _)) (exists_vector_succ f).symm
id      └──┘        └───────┘  └──────────┘     └──────────────────┘      └────────────────┘   └──┘
src     └──┘         └───────┘  └──────────┘                                └────────────────┘   └──┘
typ     └──┘        └───────┘  └──────────┘     └──────────────────┘      └────────────────┘   └──┘
233  
234  theorem vector_all_iff_forall {α} : ∀ {n} (f : vector3 α n → Prop), vector_all n f ↔ ∀ v, f v
id                                                └─────┘           └────────┘         
src                                                 └─────┘              └────────┘     
typ                                               └─────┘           └────────┘         
doc                                                 └─────┘              └────────┘
235  | 0        f := ⟨λf0 v, v.nil_elim f0, λal, al []⟩
id                     └┘   └───────┘ └┘   └┘  └┘ └┘
src                           └───────┘             └┘
typ                    └┘   └───────┘ └┘   └┘  └┘ └┘
doc                                                 └┘
236  | (succ n) f := (forall_congr (λx, vector_all_iff_forall (λv, f (x :: v)))).trans
id      └──┘         └──────────┘     └───────────────────┘         └┘     └───┘
src     └──┘          └──────────┘                                      └┘      └───┘
typ     └──┘         └──────────┘     └───────────────────┘         └┘     └───┘
doc                                                                     └┘
237    ⟨λal v, v.cons_elim al, λal x v, al (x::v)⟩
id       └┘   └────────┘ └┘   └┘    └┘  └┘
src             └────────┘                   └┘
typ      └┘   └────────┘ └┘   └┘    └┘  └┘
doc                                          └┘
238  
239  /-- `vector_allp p v` is equivalent to `∀ i, p (v i)`, but unfolds directly to a conjunction,
240    i.e. `vector_allp p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/
241  def vector_allp {α} (p : α → Prop) {n} (v : vector3 α n) : Prop :=
id                                              └─────┘  
src                                              └─────┘
typ                                             └─────┘  
doc                                              └─────┘
242  vector3.rec_on v true (λn a v IH, @vector3.rec_on _ (λn v, Prop) _ v (p a) (λn b v' _, p a ∧ IH))
id   └────────────┘  └──┘      └┘   └────────────┘                         └┘      └┘
src  └────────────┘   └──┘              └────────────┘                                          
typ  └────────────┘  └──┘      └┘   └────────────┘                         └┘      └┘
243  
244  @[simp] theorem vector_allp_nil {α} (p : α → Prop) : vector_allp p [] = true := rfl
id                                                       └─────────┘  └┘  └──┘    └─┘
src                                                       └─────────┘   └┘  └──┘    └─┘
typ                                                      └─────────┘  └┘  └──┘    └─┘
doc    └──┘                                               └─────────┘   └┘
245  @[simp] theorem vector_allp_singleton {α} (p : α → Prop) (x : α) : vector_allp p [x] = p x := rfl
id                                                                    └─────────┘         └─┘
src                                                                     └─────────┘             └─┘
typ                                                                   └─────────┘         └─┘
doc    └──┘                                                             └─────────┘    
246  @[simp] theorem vector_allp_cons {α} (p : α → Prop) {n} (x : α) (v : vector3 α n) :
id                                                                      └─────┘  
src                                                                       └─────┘
typ                                                                     └─────┘  
doc    └──┘                                                               └─────┘
247    vector_allp p (x :: v) ↔ p x ∧ vector_allp p v :=
id     └─────────┘    └┘       └─────────┘  
src    └─────────┘      └┘          └─────────┘
typ    └─────────┘    └┘       └─────────┘  
doc    └─────────┘      └┘            └─────────┘
248  vector3.rec_on v (and_true _).symm (λn a v IH, iff.rfl)
id   └────────────┘   └──────┘   └──┘       └┘  └─────┘
src  └────────────┘    └──────┘   └──┘              └─────┘
typ  └────────────┘   └──────┘   └──┘       └┘  └─────┘
249  
250  theorem vector_allp_iff_forall {α} (p : α → Prop) {n} (v : vector3 α n) : vector_allp p v ↔ ∀ i, p (v i) :=
id                                                             └─────┘      └─────────┘           
src                                                             └─────┘        └─────────┘     
typ                                                            └─────┘      └─────────┘           
doc                                                             └─────┘        └─────────┘
251  begin refine v.rec_on _ _,
id                └──────┘
src        └─────┘└──────┘└──┘
typ        └─────┘└──────┘└──┘
doc        └─────┘        └──┘
txt        └─────┘        └──┘
par        └─────┘        └──┘
pid                      └──┘
st   └───────────────────────┘└─
252    { exact ⟨λ_, fin2.elim0, λ_, trivial⟩ },
id                  └────────┘      └─────┘
src      └────┘  └─┘└────────┘└┘ └─┘└─────┘└┘
typ      └────┘  └─┘└────────┘└┘ └─┘└─────┘└┘
doc      └────┘  └─┘          └┘ └─┘       └┘
txt      └────┘  └─┘          └┘ └─┘       └┘
par      └────┘  └─┘          └┘ └─┘       └┘
pid             └─┘          └┘ └─┘       
st   ───┘└──────────────────────────────────┘└┘
253    { simp, refine λn a v IH, (and_congr_right (λ_, IH)).trans
id                                └─────────────┘
src      └──┘  └─────┘ └────────┘ └─────────────┘  └─┘  └────────
typ      └──┘  └─────┘ └────────┘ └─────────────┘  └─┘  └────────
doc      └──┘  └─────┘ └────────┘                  └─┘  └────────
txt      └──┘  └─────┘ └────────┘                  └─┘  └────────
par      └──┘  └─────┘ └────────┘                  └─┘  └────────
pid                   └────────┘                  └─┘  └────────
st   ───────┘└────────────────────────────────────────────────────
254        ⟨λ⟨pa, h⟩ i, by {refine i.cases' _ _, exacts [pa, h]}, λh, ⟨_, λi, _⟩⟩,
id                                 └──────┘              └┘  
src  ─────┘    └┘ └───┘  └───────┘└──────┘└────┘└──────┘  └┘ └─┘ └─┘ └─┘ └────┘
typ  ─────┘    └┘ └───┘  └───────┘└──────┘└────┘└──────┘└┘└┘└─┘ └─┘ └─┘ └────┘
doc  ─────┘    └┘ └───┘  └───────┘        └────┘└──────┘  └┘ └─┘ └─┘ └─┘ └────┘
txt  ─────┘    └┘ └───┘  └───────┘        └────┘└──────┘  └┘ └─┘ └─┘ └─┘ └────┘
par  ─────┘    └┘ └───┘  └───────┘        └────┘└──────┘  └┘ └─┘ └─┘ └─┘ └────┘
pid  ─────┘    └┘ └───┘  └───────┘        └────────────┘  └┘ └──┘ └─┘ └─┘ └────┘
st   ────────────────────┘└───────────────────┘└──────────────┘└───────────────┘└─
255      { have h0 := h fz, simp at h0, exact h0 },
id                     └┘                    └┘
src        └─────────┘ └┘  └────────┘  └────┘  
typ        └─────────┘└┘  └────────┘  └────┘└┘
doc        └─────────┘     └────────┘  └────┘  
txt        └─────────┘     └────────┘  └────┘  
par        └─────────┘     └────────┘  └────┘  
pid        └─────┘└─┘         └───┘         
st   ─────┘└─────────────┘└──────────┘└─────────┘└┘
256      { have hs := h (fs i), simp at hs, exact hs } }
id                      └┘                      └┘
src        └─────────┘  └┘   └────────┘  └────┘  
typ        └─────────┘ └┘  └────────┘  └────┘└┘
doc        └─────────┘       └────────┘  └────┘  
txt        └─────────┘       └────────┘  └────┘  
par        └─────────┘       └────────┘  └────┘  
pid        └─────┘└─┘           └───┘         
st   ────────────────────────┘└──────────┘└─────────┘└───
257  end
st   ──┘
258  
259  theorem vector_allp.imp {α} {p q : α → Prop} (h : ∀ x, p x → q x)
id                                                             
typ                                                            
260    {n} {v : vector3 α n} (al : vector_allp p v) : vector_allp q v :=
id              └─────┘          └─────────┘      └─────────┘  
src             └─────┘            └─────────┘        └─────────┘
typ             └─────┘          └─────────┘      └─────────┘  
doc             └─────┘            └─────────┘        └─────────┘
261  (vector_allp_iff_forall _ _).2 (λi, h _ $ (vector_allp_iff_forall _ _).1 al _)
id    └────────────────────┘                 └────────────────────┘       └┘
src   └────────────────────┘                   └────────────────────┘     
typ   └────────────────────┘                 └────────────────────┘       └┘
262  end vector3
263  
264  /-- `list_all p l` is equivalent to `∀ a ∈ l, p a`, but unfolds directly to a conjunction,
265    i.e. `list_all p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/
266  @[simp] def list_all {α} (p : α → Prop) : list α → Prop
id                                            └──┘  
src                                            └──┘
typ                                           └──┘  
doc    └──┘
267  | []        := true
id     └┘           └──┘
src    └┘           └──┘
typ    └┘           └──┘
268  | (x :: []) := p x
id       └┘ └┘     
src       └┘ └┘
typ      └┘ └┘     
269  | (x :: l)  := p x ∧ list_all l
id       └┘           └──────┘
src       └┘            
typ      └┘           └──────┘
270  
271  @[simp] theorem list_all_cons {α} (p : α → Prop) (x : α) : ∀ (l : list α), list_all p (x :: l) ↔ p x ∧ list_all p l
id                                                                  └──┘    └──────┘    └┘       └──────┘  
src                                                                    └──┘     └──────┘      └┘          └──────┘
typ                                                                 └──┘    └──────┘    └┘       └──────┘  
doc    └──┘                                                                     └──────┘                    └──────┘
272  | []       := (and_true _).symm
id     └┘           └──────┘   └──┘
src    └┘           └──────┘   └──┘
typ    └┘           └──────┘   └──┘
273  | (x :: l) := iff.rfl
id        └┘       └─────┘
src       └┘       └─────┘
typ       └┘       └─────┘
274  
275  theorem list_all_iff_forall {α} (p : α → Prop) : ∀ (l : list α), list_all p l ↔ ∀ x ∈ l, p x
id                                                         └──┘    └──────┘            
src                                                          └──┘     └──────┘        
typ                                                        └──┘    └──────┘            
doc                                                                   └──────┘
276  | []       := (iff_true_intro $ list.ball_nil _).symm
id     └┘           └────────────┘   └───────────┘   └──┘
src    └┘           └────────────┘   └───────────┘   └──┘
typ    └┘           └────────────┘   └───────────┘   └──┘
277  | (x :: l) := by rw [list.ball_cons, ← list_all_iff_forall l]; simp
id        └┘              └────────────┘    └─────────────────┘ 
src       └┘          └──┘└────────────┘└──┘                      └────
typ       └┘          └──┘└────────────┘└──┘└─────────────────┘  └────
doc                   └──┘              └──┘                      └────
txt                   └──┘              └──┘                      └────
par                   └──┘              └──┘                      └────
pid                     └┘              └──┘                          
st                   └─────────────────┘└───────────────────────┘└──────
278  
src  
typ  
doc  
txt  
par  
pid  
st   
279  theorem list_all.imp {α} {p q : α → Prop} (h : ∀ x, p x → q x) : ∀ {l : list α}, list_all p l → list_all q l
id                                                                    └──┘    └──────┘     └──────┘  
src                                                                          └──┘     └──────┘       └──────┘
typ                                                                   └──┘    └──────┘     └──────┘  
doc                                                                                   └──────┘       └──────┘
280  | []       := id
id     └┘          └┘
src    └┘          └┘
typ    └┘          └┘
281  | (x :: l) := by simpa using and.imp (h x) list_all.imp
id        └┘                      └─────┘     └──────────┘
src       └┘          └──────────┘└─────┘   └┘            
typ       └┘          └──────────┘└─────┘ └┘└──────────┘
doc                   └──────────┘          └┘            
txt                   └──────────┘          └┘            
par                   └──────────┘          └┘            
pid                        └────┘          └┘            
st                   └───────────────────────────────────────
282  
src  
typ  
doc  
txt  
par  
pid  
st   
283  @[simp] theorem list_all_map {α β} {p : β → Prop} (f : α → β) {l : list α} : list_all p (l.map f) ↔ list_all (p ∘ f) l :=
id                                                                   └──┘     └──────┘   └──┘    └──────┘      
src                                                                     └──┘      └──────┘     └──┘     └──────┘    
typ                                                                  └──┘     └──────┘   └──┘    └──────┘      
doc    └──┘                                                                       └──────┘               └──────┘
284  by induction l; simp *
id                
src     └────────┘   └──────
typ     └────────┘  └──────
doc     └────────┘   └──────
txt     └────────┘   └──────
par     └────────┘   └──────
pid                     
st     └────────────────────
285  
src  
typ  
doc  
txt  
par  
pid  
st   
286  theorem list_all_congr {α} {p q : α → Prop} (h : ∀ x, p x ↔ q x) {l : list α} : list_all p l ↔ list_all q l :=
id                                                                  └──┘     └──────┘    └──────┘  
src                                                                       └──┘      └──────┘      └──────┘
typ                                                                 └──┘     └──────┘    └──────┘  
doc                                                                                  └──────┘       └──────┘
287  ⟨list_all.imp (λx, (h x).1), list_all.imp (λx, (h x).2)⟩
id    └──────────┘            └──────────┘        
src   └──────────┘               └──────────┘           
typ   └──────────┘            └──────────┘        
288  
289  instance decidable_list_all {α} (p : α → Prop) [decidable_pred p] (l : list α) : decidable (list_all p l) :=
id                                                  └────────────┘        └──┘     └───────┘  └──────┘  
src                                                  └────────────┘         └──┘      └───────┘  └──────┘
typ                                                 └────────────┘        └──┘     └───────┘  └──────┘  
doc                                                                                              └──────┘
290  decidable_of_decidable_of_iff (by apply_instance) (list_all_iff_forall _ _).symm
id   └───────────────────────────┘                      └─────────────────┘     └──┘
src  └───────────────────────────┘     └────────────┘   └─────────────────┘     └──┘
typ  └───────────────────────────┘     └────────────┘   └─────────────────┘     └──┘
doc                                    └────────────┘
txt                                    └────────────┘
par                                    └────────────┘
st                                    └─────────────┘
291  
292  /- poly -/
293  
294  /-- A predicate asserting that a function is a multivariate integer polynomial.
295    (We are being a bit lazy here by allowing many representations for multiplication,
296    rather than only allowing monomials and addition, but the definition is equivalent
297    and this is easier to use.) -/
298  inductive is_poly {α} : ((α → ℕ) → ℤ) → Prop
id                                   
src                                    
typ                                  
299  | proj : ∀ i, is_poly (λx : α → ℕ, x i)
id                                    
src                                  
typ                                   
300  | const : Π (n : ℤ), is_poly (λx : α → ℕ, n)
id                                          
src                                        
typ                                         
301  | sub : Π {f g : (α → ℕ) → ℤ}, is_poly f → is_poly g → is_poly (λx, f x - g x)
id                              └─────┘    └─────┘                    
src                                                                        
typ                             └─────┘    └─────┘                    
302  | mul : Π {f g : (α → ℕ) → ℤ}, is_poly f → is_poly g → is_poly (λx, f x * g x)
id                              └─────┘    └─────┘                    
src                                                                        
typ                             └─────┘    └─────┘                    
303  
304  /-- The type of multivariate integer polynomials -/
305  def poly (α : Type u) := {f : (α → ℕ) → ℤ // is_poly f}
id                                          └─────┘ 
src                                            └─────┘
typ                                         └─────┘ 
doc                                               └─────┘
306  
307  namespace poly
308  section
309  parameter {α : Type u}
310  
311  instance : has_coe_to_fun (poly α) := ⟨_, λ f, f.1⟩
id              └────────────┘  └──┘              
src             └────────────┘  └──┘                 
typ             └────────────┘  └──┘              
doc                             └──┘
312  
313  /-- The underlying function of a `poly` is a polynomial -/
314  lemma isp (f : poly α) : is_poly f := f.2
id                  └──┘     └─────┘     
src                 └──┘      └─────┘       
typ                 └──┘     └─────┘     
doc                 └──┘      └─────┘
315  
316  /-- Extensionality for `poly α` -/
317  lemma ext {f g : poly α} (e : ∀x, f x = g x) : f = g :=
id                    └──┘                     
src                   └──┘                           
typ                   └──┘                     
doc                   └──┘
318  subtype.eq (funext e)
id   └────────┘  └────┘ 
src  └────────┘  └────┘
typ  └────────┘  └────┘ 
319  
320  /-- Construct a `poly` given an extensionally equivalent `poly`. -/
321  def subst (f : poly α) (g : (α → ℕ) → ℤ) (e : ∀x, f x = g x) : poly α :=
id                  └──┘                                 └──┘ 
src                 └──┘                                         └──┘
typ                 └──┘                                 └──┘ 
doc                 └──┘                                            └──┘
322  ⟨g, by rw ← (funext e : coe_fn f = g); exact f.isp⟩
id               └────┘    └────┘            └───┘
src         └───┘ └────┘ └─┘└────┘    └────┘└───┘
typ        └───┘ └────┘└─┘└────┘  └────┘└───┘
doc         └───┘        └─┘           └────┘└───┘
txt         └───┘        └─┘           └────┘
par         └───┘        └─┘           └────┘
pid           └─┘        └─┘                
st         └──────────────────────────────────────────┘
323  @[simp] theorem subst_eval (f g e x) : subst f g e x = g x := rfl
id                                          └───┘           └─┘
src                                         └───┘                 └─┘
typ                                         └───┘           └─┘
doc    └──┘                                 └───┘
324  
325  /-- The `i`th projection function, `x_i`. -/
326  def proj (i) : poly α := ⟨_, is_poly.proj i⟩
id                  └──┘         └──────────┘ 
src                 └──┘          └──────────┘
typ                 └──┘         └──────────┘ 
doc                 └──┘
327  @[simp] theorem proj_eval (i x) : proj i x = x i := rfl
id                                     └──┘         └─┘
src                                    └──┘             └─┘
typ                                    └──┘         └─┘
doc    └──┘                            └──┘
328  
329  /-- The constant function with value `n : ℤ`. -/
330  def const (n) : poly α := ⟨_, is_poly.const n⟩
id                   └──┘         └───────────┘ 
src                  └──┘          └───────────┘
typ                  └──┘         └───────────┘ 
doc                  └──┘
331  @[simp] theorem const_eval (n x) : const n x = n := rfl
id                                      └───┘        └─┘
src                                     └───┘           └─┘
typ                                     └───┘        └─┘
doc    └──┘                             └───┘
332  
333  /-- The zero polynomial -/
334  def zero : poly α := const 0
id              └──┘     └───┘
src             └──┘      └───┘
typ             └──┘     └───┘
doc             └──┘      └───┘
335  instance : has_zero (poly α) := ⟨poly.zero⟩
id              └──────┘  └──┘       └───────┘
src             └──────┘  └──┘        └───────┘
typ             └──────┘  └──┘       └───────┘
doc                       └──┘        └───────┘
336  @[simp] theorem zero_eval (x) : (0 : poly α) x = 0 := rfl
id                                        └──┘          └─┘
src                                       └──┘            └─┘
typ                                       └──┘          └─┘
doc    └──┘                               └──┘
337  
338  /-- The zero polynomial -/
339  def one : poly α := const 1
id             └──┘     └───┘
src            └──┘      └───┘
typ            └──┘     └───┘
doc            └──┘      └───┘
340  instance : has_one (poly α) := ⟨poly.one⟩
id              └─────┘  └──┘       └──────┘
src             └─────┘  └──┘        └──────┘
typ             └─────┘  └──┘       └──────┘
doc                      └──┘        └──────┘
341  @[simp] theorem one_eval (x) : (1 : poly α) x = 1 := rfl
id                                       └──┘          └─┘
src                                      └──┘            └─┘
typ                                      └──┘          └─┘
doc    └──┘                              └──┘
342  
343  /-- Subtraction of polynomials -/
344  def sub : poly α → poly α → poly α | ⟨f, pf⟩ ⟨g, pg⟩ :=
id             └──┘   └──┘    └──┘        └┘      └┘
src            └──┘     └──┘     └──┘
typ            └──┘   └──┘    └──┘        └┘      └┘
doc            └──┘     └──┘     └──┘
345  ⟨_, is_poly.sub pf pg⟩
id       └─────────┘
src      └─────────┘
typ      └─────────┘
346  instance : has_sub (poly α) := ⟨poly.sub⟩
id              └─────┘  └──┘       └──────┘
src             └─────┘  └──┘        └──────┘
typ             └─────┘  └──┘       └──────┘
doc                      └──┘        └──────┘
347  @[simp] theorem sub_eval : Π (f g x), (f - g : poly α) x = f x - g x
id                                           └──┘         
src                                                └──┘           
typ                                          └──┘         
doc    └──┘                                         └──┘
348  | ⟨f, pf⟩ ⟨g, pg⟩ x := rfl
id                          └─┘
src                         └─┘
typ                         └─┘
349  
350  /-- Negation of a polynomial -/
351  def neg (f : poly α) : poly α := 0 - f
id                └──┘     └──┘        
src               └──┘      └──┘        
typ               └──┘     └──┘        
doc               └──┘      └──┘
352  instance : has_neg (poly α) := ⟨poly.neg⟩
id              └─────┘  └──┘       └──────┘
src             └─────┘  └──┘        └──────┘
typ             └─────┘  └──┘       └──────┘
doc                      └──┘        └──────┘
353  @[simp] theorem neg_eval (f x) : (-f : poly α) x = -f x :=
id                                        └──┘      
src                                        └──┘       
typ                                       └──┘      
doc    └──┘                                 └──┘
354  show (0-f) x = _, by simp
id             
src                     └────
typ                   └────
doc                       └────
txt                       └────
par                       └────
pid                           
st                       └─────
355  
src  
typ  
doc  
txt  
par  
pid  
st   
356  /-- Addition of polynomials -/
357  def add : poly α → poly α → poly α | ⟨f, pf⟩ ⟨g, pg⟩ :=
id             └──┘   └──┘    └──┘       └┘     └┘
src            └──┘     └──┘     └──┘
typ            └──┘   └──┘    └──┘       └┘     └┘
doc            └──┘     └──┘     └──┘
358  subst (⟨f, pf⟩ - -⟨g, pg⟩) _
id   └───┘           
src  └───┘           
typ  └───┘           
doc  └───┘
359   (λx, show f x - (0 - g x) = f x + g x, by simp)
id                                
src                                         └──┘
typ                                    └──┘
doc                                             └──┘
txt                                             └──┘
par                                             └──┘
st                                             └───┘
360  instance : has_add (poly α) := ⟨poly.add⟩
id              └─────┘  └──┘       └──────┘
src             └─────┘  └──┘        └──────┘
typ             └─────┘  └──┘       └──────┘
doc                      └──┘        └──────┘
361  @[simp] theorem add_eval : Π (f g x), (f + g : poly α) x = f x + g x
id                                           └──┘         
src                                                └──┘           
typ                                          └──┘         
doc    └──┘                                         └──┘
362  | ⟨f, pf⟩ ⟨g, pg⟩ x := rfl
id                          └─┘
src                         └─┘
typ                         └─┘
363  
364  /-- Multiplication of polynomials -/
365  def mul : poly α → poly α → poly α | ⟨f, pf⟩ ⟨g, pg⟩ :=
id             └──┘   └──┘    └──┘        └┘      └┘
src            └──┘     └──┘     └──┘
typ            └──┘   └──┘    └──┘        └┘      └┘
doc            └──┘     └──┘     └──┘
366  ⟨_, is_poly.mul pf pg⟩
id       └─────────┘
src      └─────────┘
typ      └─────────┘
367  instance : has_mul (poly α) := ⟨poly.mul⟩
id              └─────┘  └──┘       └──────┘
src             └─────┘  └──┘        └──────┘
typ             └─────┘  └──┘       └──────┘
doc                      └──┘        └──────┘
368  @[simp] theorem mul_eval : Π (f g x), (f * g : poly α) x = f x * g x
id                                           └──┘         
src                                                └──┘           
typ                                          └──┘         
doc    └──┘                                         └──┘
369  | ⟨f, pf⟩ ⟨g, pg⟩ x := rfl
id                          └─┘
src                         └─┘
typ                         └─┘
370  
371  instance : comm_ring (poly α) := by refine
id              └───────┘  └──┘ 
src             └───────┘  └──┘          └─────┘
typ             └───────┘  └──┘         └─────┘
doc                        └──┘          └─────┘
txt                                      └─────┘
par                                      └─────┘
pid                                            
st                                      └───────
372  { add  := (+),
id             
src   └───────┘└───
typ   └───────┘└───
doc   └───────┘ └───
txt   └───────┘ └───
par   └───────┘ └───
pid   └───────┘ └───
st   ───────────────
373    zero := 0,
src  ─────────────
typ  ─────────────
doc  ─────────────
txt  ─────────────
par  ─────────────
pid  ─────────────
st   ─────────────
374    neg  := has_neg.neg,
id             └─────────┘
src  ─────────┘└─────────┘└─
typ  ─────────┘└─────────┘└─
doc  ─────────┘           └─
txt  ─────────┘           └─
par  ─────────┘           └─
pid  ─────────┘           └─
st   ───────────────────────
375    mul  := (*),
id             
src  ─────────┘└───
typ  ─────────┘└───
doc  ─────────┘ └───
txt  ─────────┘ └───
par  ─────────┘ └───
pid  ─────────┘ └───
st   ───────────────
376    one  := 1, .. }; {intros, exact ext (λx, by simp [mul_add, mul_left_comm, mul_comm])}
id                                     └─┘               └─────┘  └───────────┘  └──────┘
src  ────────────────┘   └────┘  └────┘└─┘  └─┘  └────┘└─────┘└┘└───────────┘└┘└──────┘
typ  ────────────────┘   └────┘  └────┘└─┘  └─┘  └────┘└─────┘└┘└───────────┘└┘└──────┘
doc  ────────────────┘   └────┘  └────┘└─┘  └─┘  └────┘       └┘             └┘        
txt  ────────────────┘   └────┘  └────┘     └─┘  └────┘       └┘             └┘        
par  ────────────────┘   └────┘  └────┘     └─┘  └────┘       └┘             └┘        
pid  ────────────────┘                     └─┘  └─────┘       └┘             └┘        └┘
st   ──────────────────┘└─────┘└─────────────────┘└──────────────────────────────────────┘└┘
377  
378  lemma induction {C : poly α → Prop}
id                        └──┘ 
src                       └──┘
typ                       └──┘ 
doc                       └──┘
379    (H1 : ∀i, C (proj i)) (H2 : ∀n, C (const n))
id                └──┘               └───┘ 
src                 └──┘                  └───┘
typ               └──┘               └───┘ 
doc                 └──┘                  └───┘
380    (H3 : ∀f g, C f → C g → C (f - g))
id                           
src                                 
typ                          
381    (H4 : ∀f g, C f → C g → C (f * g)) (f : poly α) : C f :=
id                                   └──┘      
src                                           └──┘
typ                                  └──┘      
doc                                            └──┘
382  begin
st   └─────
383    cases f with f pf,
id           
src    └────┘ └────────┘
typ    └────┘└────────┘
doc    └────┘ └────────┘
txt    └────┘ └────────┘
par    └────┘ └────────┘
pid          └────────┘
st   ──────────────────┘└─
384    induction pf with i n f g pf pg ihf ihg f g pf pg ihf ihg,
id               └┘
src    └────────┘  └───────────────────────────────────────────┘
typ    └────────┘└┘└───────────────────────────────────────────┘
doc    └────────┘  └───────────────────────────────────────────┘
txt    └────────┘  └───────────────────────────────────────────┘
par    └────────┘  └───────────────────────────────────────────┘
pid               └──────────────────────────────────────────┘
st   ──────────────────────────────────────────────────────────┘└─
385    apply H1, apply H2, apply H3 _ _ ihf ihg, apply H4 _ _ ihf ihg
id                               └┘     └─┘ └─┘        └┘     └─┘ └─┘
src    └────┘    └────┘    └────┘  └───┘        └────┘  └───┘      
typ    └────┘    └────┘    └────┘└┘└───┘└─┘└─┘  └────┘└┘└───┘└─┘└─┘
doc    └────┘    └────┘    └────┘  └───┘        └────┘  └───┘      
txt    └────┘    └────┘    └────┘  └───┘        └────┘  └───┘      
par    └────┘    └────┘    └────┘  └───┘        └────┘  └───┘      
pid                             └───┘               └───┘      
st   ─────────┘└────────┘└────────────────────┘└─────────────────────┘
386  end
st   └─┘
387  
388  /-- The sum of squares of a list of polynomials. This is relevant for
389    Diophantine equations, because it means that a list of equations
390    can be encoded as a single equation: `x = 0 ∧ y = 0 ∧ z = 0` is
391    equivalent to `x^2 + y^2 + z^2 = 0`. -/
392  def sumsq : list (poly α) → poly α
id               └──┘  └──┘    └──┘ 
src              └──┘  └──┘      └──┘
typ              └──┘  └──┘    └──┘ 
doc                    └──┘      └──┘
393  | []      := 0
id     └┘
src    └┘
typ    └┘
394  | (p::ps) := p*p + sumsq ps
id      └┘└┘         └───┘
src      └┘          
typ     └┘└┘         └───┘
395  
396  theorem sumsq_nonneg (x) : ∀ l, 0 ≤ sumsq l x
id                                     └───┘  
src                                     └───┘
typ                                    └───┘  
doc                                      └───┘
397  | []      := le_refl 0
id     └┘         └─────┘
src    └┘         └─────┘
typ    └┘         └─────┘
398  | (p::ps) := by rw sumsq; simp [-add_comm];
id       └┘             └───┘
src      └┘          └─┘└───┘  └──────────────┘
typ      └┘          └─┘└───┘  └──────────────┘
doc                  └─┘└───┘  └──────────────┘
txt                  └─┘       └──────────────┘
par                  └─┘       └──────────────┘
pid                               └─────────┘
st                  └────────────────────────────
399                  exact add_nonneg (mul_self_nonneg _) (sumsq_nonneg ps)
id                         └────────┘  └─────────────┘     └──────────┘ └┘
src                  └────┘└────────┘ └─────────────┘└──┘               └─
typ                  └────┘└────────┘ └─────────────┘└──┘ └──────────┘└┘└─
doc                  └────┘                          └──┘               └─
txt                  └────┘                          └──┘               └─
par                  └────┘                          └──┘               └─
pid                                                 └──┘               
st   ───────────────────────────────────────────────────────────────────────
400  
src  
typ  
doc  
txt  
par  
pid  
st   
401  theorem sumsq_eq_zero (x) : ∀ l, sumsq l x = 0 ↔ list_all (λa : poly α, a x = 0) l
id                                   └───┘       └──────┘       └──┘         
src                                   └───┘         └──────┘       └──┘        
typ                                  └───┘       └──────┘       └──┘         
doc                                   └───┘           └──────┘       └──┘
402  | []      := eq_self_iff_true _
id     └┘         └──────────────┘
src    └┘         └──────────────┘
typ    └┘         └──────────────┘
403  | (p::ps) := by rw [list_all_cons, ← sumsq_eq_zero ps]; rw sumsq; simp [-add_comm]; exact
id       └┘              └───────────┘    └───────────┘ └┘      └───┘
src      └┘          └──┘└───────────┘└──┘                 └─┘└───┘  └──────────────┘  └─────
typ      └┘          └──┘└───────────┘└──┘└───────────┘└┘  └─┘└───┘  └──────────────┘  └─────
doc                  └──┘             └──┘                 └─┘└───┘  └──────────────┘  └─────
txt                  └──┘             └──┘                 └─┘       └──────────────┘  └─────
par                  └──┘             └──┘                 └─┘       └──────────────┘  └─────
pid                    └┘             └──┘                              └─────────┘       
st                  └────────────────┘└──────────────────┘└───┘└───┘└─────────────────────────
404    ⟨λ(h : p x * p x + sumsq ps x = 0),
id                      └───┘ └┘   
src  ─┘  └───┘    └───┘   └────
typ  ─┘  └───┘    └───┘└┘ └────
doc  ─┘  └───┘      └───┘    └────
txt  ─┘  └───┘               └────
par  ─┘  └───┘               └────
pid  ─┘  └───┘               └────
st   ──────────────────────────────────────
405     have p x = 0, from eq_zero_of_mul_self_eq_zero $ le_antisymm
id                        └─────────────────────────┘   └─────────┘
src  ──┘    └─┘  └───────┘└─────────────────────────┘ └─────────┘
typ  ──┘    └─┘ └───────┘└─────────────────────────┘ └─────────┘
doc  ──┘    └─┘  └───────┘                                       
txt  ──┘    └─┘  └───────┘                                       
par  ──┘    └─┘  └───────┘                                       
pid  ──┘    └─┘  └───────┘                                       
st   ────────────────────────────────────────────────────────────────
406       (by rw ← h; have t := add_le_add_left (sumsq_nonneg x ps) (p x * p x); rwa [add_zero] at t)
id                             └─────────────┘  └──────────┘   └┘                  └──────┘
src  ────┘   └───┘ └┘└────────┘└─────────────┘ └──────────┘   └┘      └┘└───┘└──────┘└────┘└─
typ  ────┘   └───┘└┘└────────┘└─────────────┘ └──────────┘ └┘└┘    └┘└───┘└──────┘└────┘└─
doc  ────┘   └───┘ └┘└────────┘                               └┘      └┘└───┘        └────┘└─
txt  ────┘   └───┘ └┘└────────┘                               └┘      └┘└───┘        └────┘└─
par  ────┘   └───┘ └┘└────────┘                               └┘      └┘└───┘        └────┘└─
pid  ────┘   └────┘ └──────────┘                               └┘      └──────┘        └───────
st   ───────┘└───────────────────────────────────────────────────────────────────────┘└──────┘└───┘└─
407       (mul_self_nonneg _),
id         └─────────────┘
src  ────┘ └─────────────┘└────
typ  ────┘ └─────────────┘└────
doc  ────┘                └────
txt  ────┘                └────
par  ────┘                └────
pid  ────┘                └────
st   ──────────────────────────
408     ⟨this, by simp [this] at h; exact h⟩,
id                      └──┘              
src  ──┘     └┘  └────┘    └────┘└──────┘ └──
typ  ──┘     └┘  └────┘└──┘└────┘└──────┘└──
doc  ──┘     └┘  └────┘    └────┘└──────┘ └──
txt  ──┘     └┘  └────┘    └────┘└──────┘ └──
par  ──┘     └┘  └────┘    └────┘└──────┘ └──
pid  ──┘     └┘  └─────┘    └────────────┘ └──
st   ───────────┘└────────────────────────┘└──
409    λ⟨h1, h2⟩, by rw [h1, h2]; refl⟩
id                       └┘  └┘
src  ─┘   └┘  └─┘  └──┘  └┘  └┘└──┘└─
typ  ─┘   └┘  └─┘  └──┘└┘└┘└┘└┘└──┘└─
doc  ─┘   └┘  └─┘  └──┘  └┘  └┘└──┘└─
txt  ─┘   └┘  └─┘  └──┘  └┘  └┘└──┘└─
par  ─┘   └┘  └─┘  └──┘  └┘  └┘└──┘└─
pid  ─┘   └┘  └─┘  └───┘  └┘  └──────┘
st   ──────────────┘└─────┘└──┘└────┘└─
410  
src  
typ  
doc  
txt  
par  
pid  
st   
411  end
412  
413  /-- Map the index set of variables, replacing `x_i` with `x_(f i)`. -/
414  def remap {α β} (f : α → β) (g : poly α) : poly β :=
id                                  └──┘     └──┘ 
src                                   └──┘      └──┘
typ                                 └──┘     └──┘ 
doc                                   └──┘      └──┘
415  ⟨λv, g $ v ∘ f, g.induction
id              └────────┘
src                  └────────┘
typ             └────────┘
416    (λi, by simp; apply is_poly.proj)
id                        └──────────┘
src            └──┘  └────┘└──────────┘
typ           └──┘  └────┘└──────────┘
doc            └──┘  └────┘
txt            └──┘  └────┘
par            └──┘  └────┘
pid                       
st            └───────────────────────┘
417    (λn, by simp; apply is_poly.const)
id                        └───────────┘
src            └──┘  └────┘└───────────┘
typ           └──┘  └────┘└───────────┘
doc            └──┘  └────┘
txt            └──┘  └────┘
par            └──┘  └────┘
pid                       
st            └────────────────────────┘
418    (λf g pf pg, by simp; apply is_poly.sub pf pg)
id         └┘ └┘                 └─────────┘ └┘ └┘
src                    └──┘  └────┘└─────────┘  
typ        └┘ └┘     └──┘  └────┘└─────────┘└┘└┘
doc                    └──┘  └────┘             
txt                    └──┘  └────┘             
par                    └──┘  └────┘             
pid                                            
st                    └────────────────────────────┘
419    (λf g pf pg, by simp; apply is_poly.mul pf pg)⟩
id         └┘ └┘                 └─────────┘ └┘ └┘
src                    └──┘  └────┘└─────────┘  
typ        └┘ └┘     └──┘  └────┘└─────────┘└┘└┘
doc                    └──┘  └────┘             
txt                    └──┘  └────┘             
par                    └──┘  └────┘             
pid                                            
st                    └────────────────────────────┘
420  @[simp] theorem remap_eval {α β} (f : α → β) (g : poly α) (v) : remap f g v = g (v ∘ f) := rfl
id                                                   └──┘         └───┘              └─┘
src                                                    └──┘          └───┘                    └─┘
typ                                                  └──┘         └───┘              └─┘
doc    └──┘                                            └──┘          └───┘
421  
422  end poly
423  
424  namespace sum
425  
426  /-- combine two functions into a function on the disjoint union -/
427  def join {α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ :=
id                                               
src                                               
typ                                              
428  by {refine sum.rec _ _, exacts [f, g]}
id              └─────┘                
src      └─────┘└─────┘└──┘  └──────┘ └┘ 
typ      └─────┘└─────┘└──┘  └──────┘└┘
doc      └─────┘       └──┘  └──────┘ └┘ 
txt      └─────┘       └──┘  └──────┘ └┘ 
par      └─────┘       └──┘  └──────┘ └┘ 
pid                   └──┘        └┘ └┘ 
st     └──────────────────┘└─────────────┘└┘
429  
430  end sum
431  
432  local infixr ` ⊗ `:65 := sum.join
id                            └──────┘
src                           └──────┘
typ                           └──────┘
doc                           └──────┘
433  
434  open sum
435  
436  namespace option
437  
438  /-- Functions from `option` can be combined similarly to `vector.cons` -/
439  def cons {α β} (a : β) (v : α → β) : option α → β :=
id                                     └────┘    
src                                       └────┘
typ                                    └────┘    
440  by {refine option.rec _ _, exacts [a, v]}
id              └────────┘                
src      └─────┘└────────┘└──┘  └──────┘ └┘ 
typ      └─────┘└────────┘└──┘  └──────┘└┘
doc      └─────┘          └──┘  └──────┘ └┘ 
txt      └─────┘          └──┘  └──────┘ └┘ 
par      └─────┘          └──┘  └──────┘ └┘ 
pid                      └──┘        └┘ └┘ 
st     └─────────────────────┘└─────────────┘└┘
441  
442  notation a :: b := cons a b
id                      └──┘
src                     └──┘
typ                     └──┘
doc                     └──┘
443  
444  @[simp] theorem cons_head_tail {α β} (v : option α → β) : v none :: v ∘ some = v :=
id                                             └────┘         └──┘ └┘   └──┘  
src                                            └────┘            └──┘ └┘    └──┘ 
typ                                            └────┘         └──┘ └┘   └──┘  
doc    └──┘                                                           └┘
445  funext $ λo, by cases o; refl
id   └────┘               
src  └────┘          └────┘   └───┘
typ  └────┘         └────┘  └───┘
doc                  └────┘   └───┘
txt                  └────┘   └───┘
par                  └────┘   └───┘
pid                              
st                  └─────────────┘
446  end option
447  
448  /- dioph -/
449  
450  /-- A set `S ⊆ ℕ^α` is diophantine if there exists a polynomial on
451    `α ⊕ β` such that `v ∈ S` iff there exists `t : ℕ^β` with `p (v, t) = 0`. -/
452  def dioph {α : Type u} (S : set (α → ℕ)) : Prop :=
id                               └─┘     
src                              └─┘      
typ                              └─┘     
453  ∃ {β : Type u} (p : poly (α ⊕ β)), ∀ (v : α → ℕ), S v ↔ ∃t, p (v ⊗ t) = 0
id         └──┘         └──┘                             
src                     └──┘                                       
typ        └──┘         └──┘                             
doc                      └──┘                                         
454  
455  namespace dioph
456  section
457    variables {α β γ : Type u}
458    theorem ext {S S' : set (α → ℕ)} (d : dioph S) (H : ∀v, S v ↔ S' v) : dioph S' :=
id                         └─┘             └───┘              └┘     └───┘ └┘
src                        └─┘              └───┘                          └───┘
typ                        └─┘             └───┘              └┘     └───┘ └┘
doc                                          └───┘                           └───┘
459    eq.rec d $ show S = S', from set.ext H
id     └────┘           └┘       └─────┘ 
src    └────┘                      └─────┘
typ    └────┘           └┘       └─────┘ 
460  
461    theorem of_no_dummies (S : set (α → ℕ)) (p : poly α) (h : ∀ (v : α → ℕ), S v ↔ p v = 0) : dioph S :=
id                                └─┘             └──┘                               └───┘ 
src                               └─┘              └──┘                                      └───┘
typ                               └─┘             └──┘                               └───┘ 
doc                                                 └──┘                                         └───┘
462    ⟨ulift empty, p.remap inl, λv, (h v).trans
id      └───┘ └───┘  └────┘ └─┘        └───┘
src     └───┘ └───┘   └────┘ └─┘           └───┘
typ     └───┘ └───┘  └────┘ └─┘        └───┘
doc     └───┘         └────┘
463      ⟨λh, ⟨λt, empty.rec _ t.down, by simp; rw [
id               └───────┘   └───┘
src                └───────┘    └───┘     └──┘  └────
typ              └───────┘   └───┘     └──┘  └────
doc                                       └──┘  └────
txt                                       └──┘  └────
par                                       └──┘  └────
pid                                               └──
st                                       └─────────┘
464        show (v ⊗ λt:ulift empty, empty.rec _ t.down) ∘ inl = v, from rfl, h]⟩,
id                     └───┘ └───┘  └───────┘    └───┘   └─┘         └─┘  
src  ─────┘       └┘└───┘└───┘└┘└───────┘└─┘ └───┘└┘└─┘ └─────┘└─┘└┘ 
typ  ─────┘       └┘└───┘└───┘└┘└───────┘└─┘ └───┘└┘└─┘└─────┘└─┘└┘
doc  ─────┘       └┘└───┘     └┘         └─┘      └┘      └─────┘   └┘ 
txt  ─────┘        └┘          └┘         └─┘      └┘      └─────┘   └┘ 
par  ─────┘        └┘          └┘         └─┘      └┘      └─────┘   └┘ 
pid  ─────┘        └┘          └┘         └─┘      └┘      └─────┘   └┘ 
st   ──────────────────────────────────────────────────────────────────────┘└─┘
465      λ⟨t, ht⟩, by simp at ht; rwa [show (v ⊗ t) ∘ inl = v, from rfl] at ht⟩⟩
id                                                  └─┘         └─┘
src                   └────────┘  └───┘        └┘ └─┘  └─────┘└─┘└─────┘
typ                  └────────┘  └───┘       └┘ └─┘└─────┘└─┘└─────┘
doc                   └────────┘  └───┘        └┘      └─────┘   └─────┘
txt                   └────────┘  └───┘        └┘      └─────┘   └─────┘
par                   └────────┘  └───┘        └┘      └─────┘   └─────┘
pid                       └───┘     └┘        └┘      └─────┘   └────┘
st                   └────────────────┘└──────────────────────────────┘└────┘
466  
467    lemma inject_dummies_lem (f : β → γ) (g : γ → option β) (inv : ∀ x, g (f x) = some x)
id                                                └────┘                    └──┘ 
src                                                  └────┘                         └──┘
typ                                               └────┘                    └──┘ 
468      (p : poly (α ⊕ β)) (v : α → ℕ) : (∃t, p (v ⊗ t) = 0) ↔
id            └──┘                               
src           └──┘                                      
typ           └──┘                               
doc           └──┘                                  
469        (∃t, p.remap (inl ⊗ (inr ∘ f)) (v ⊗ t) = 0) :=
id           └────┘  └─┘   └─┘          
src            └────┘  └─┘   └─┘             
typ          └────┘  └─┘   └─┘          
doc              └────┘                     
470    begin
st     └─────
471      simp, refine ⟨λt, _, λt, _⟩; cases t with t ht,
id                                          
src      └──┘  └─────┘  └────┘ └───┘  └────┘ └────────┘
typ      └──┘  └─────┘  └────┘ └───┘  └────┘└────────┘
doc      └──┘  └─────┘  └────┘ └───┘  └────┘ └────────┘
txt      └──┘  └─────┘  └────┘ └───┘  └────┘ └────────┘
par      └──┘  └─────┘  └────┘ └───┘  └────┘ └────────┘
pid                    └────┘ └───┘        └────────┘
st   ───────┘└────────────────────────────────────────┘└─
472      { have : (v ⊗ (0 :: t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t :=
id                       └┘          └─┘   └─┘         
src        └─────┘   └┘└┘ └┘ └┘  └─┘ └─┘  └┘   └───
typ        └─────┘   └┘└┘ └┘└┘  └─┘ └─┘ └┘ └───
doc        └─────┘   └┘└┘ └┘  └┘           └┘    └───
txt        └─────┘    └┘   └┘  └┘           └┘    └───
par        └─────┘    └┘   └┘  └┘           └┘    └───
pid        └───┘└┘    └┘   └┘  └┘           └┘    └───
st   ─────┘└──────────────────────────────────────────────────────
473        funext (λs, by cases s with a b; dsimp [join, (∘)]; try {rw inv}; refl),
id         └────┘                                 └──┘               └─┘
src  ─────┘└────┘  └─┘  └────┘ └───────┘└┘└─────┘└──┘└┘└─┘└┘└───┘└─┘   └┘└──┘
typ  ─────┘└────┘  └─┘  └────┘└───────┘└┘└─────┘└──┘└┘└─┘└┘└───┘└─┘└─┘└┘└──┘
doc  ─────┘        └─┘  └────┘ └───────┘└┘└─────┘└──┘└┘ └─┘└┘└───┘└─┘   └┘└──┘
txt  ─────┘        └─┘  └────┘ └───────┘└┘└─────┘    └┘ └─┘└┘└───┘└─┘   └┘└──┘
par  ─────┘        └─┘  └────┘ └───────┘└┘└─────┘    └┘ └─┘└┘└───┘└─┘   └┘└──┘
pid  ─────┘        └─┘  └─────┘ └────────────────┘    └┘ └───────────┘   └──────┘
st   ───────────────────┘└─────────────────────────────────────────┘└────┘└────┘└─
474        exact ⟨(0 :: t) ∘ g, by rwa this⟩ },
id                                   └──┘
src        └────┘  └┘   └┘  └┘  └──┘    └┘
typ        └────┘  └┘  └┘ └┘  └──┘└──┘└┘
doc        └────┘  └┘   └┘  └┘  └──┘    └┘
txt        └────┘  └┘   └┘  └┘  └──┘    └┘
par        └────┘  └┘   └┘  └┘  └──┘    └┘
pid               └┘   └┘  └┘  └───┘    
st   ────────────────────────────┘└───────┘└┘└┘
475      { have : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f) :=
id                                     └─┘   └─┘   
src        └─────┘          └┘  └─┘ └─┘  └────
typ        └─────┘        └┘  └─┘ └─┘ └────
doc        └─────┘          └┘           └────
txt        └─────┘          └┘           └────
par        └─────┘          └┘           └────
pid        └───┘└┘          └┘           └───
st   ──────────────────────────────────────────────────────
476        funext (λs, by cases s with a b; refl),
id         └────┘               
src  ─────┘└────┘  └─┘  └────┘ └───────┘└┘└──┘
typ  ─────┘└────┘  └─┘  └────┘└───────┘└┘└──┘
doc  ─────┘        └─┘  └────┘ └───────┘└┘└──┘
txt  ─────┘        └─┘  └────┘ └───────┘└┘└──┘
par  ─────┘        └─┘  └────┘ └───────┘└┘└──┘
pid  ─────┘        └─┘  └─────┘ └──────────────┘
st   ───────────────────┘└─────────────────────┘└─
477        exact ⟨t ∘ f, by rwa this⟩ }
id                            └──┘
src        └────┘    └┘  └──┘    └┘
typ        └────┘  └┘  └──┘└──┘└┘
doc        └────┘    └┘  └──┘    └┘
txt        └────┘    └┘  └──┘    └┘
par        └────┘    └┘  └──┘    └┘
pid                 └┘  └───┘    
st   ─────────────────────┘└───────┘└┘└─
478    end
st   ────┘
479  
480    theorem inject_dummies {S : set (α → ℕ)} (f : β → γ) (g : γ → option β) (inv : ∀ x, g (f x) = some x)
id                                 └─┘                          └────┘                    └──┘ 
src                                └─┘                              └────┘                         └──┘
typ                                └─┘                          └────┘                    └──┘ 
481      (p : poly (α ⊕ β)) (h : ∀ (v : α → ℕ), S v ↔ ∃t, p (v ⊗ t) = 0) :
id            └──┘                                  
src           └──┘                                            
typ           └──┘                                  
doc           └──┘                                             
482      ∃ q : poly (α ⊕ γ), ∀ (v : α → ℕ), S v ↔ ∃t, q (v ⊗ t) = 0 :=
id            └──┘                            
src           └──┘                                      
typ           └──┘                            
doc            └──┘                                        
483    ⟨p.remap (inl ⊗ (inr ∘ f)), λv, (h v).trans $ inject_dummies_lem f g inv _ _⟩
id      └────┘  └─┘   └─┘            └───┘    └────────────────┘   └─┘
src      └────┘  └─┘   └─┘                └───┘    └────────────────┘
typ     └────┘  └─┘   └─┘            └───┘    └────────────────┘   └─┘
doc      └────┘      
484  
485    theorem reindex_dioph {S : set (α → ℕ)} : Π (d : dioph S) (f : α → β), dioph (λv, S (v ∘ f))
id                                └─┘                └───┘             └───┘         
src                               └─┘                  └───┘                 └───┘           
typ                               └─┘                └───┘             └───┘         
doc                                                     └───┘                 └───┘
486    | ⟨γ, p, pe⟩ f := ⟨γ, p.remap ((inl ∘ f) ⊗ inr), λv, (pe _).trans $ exists_congr $ λt,
id            └┘           └────┘   └─┘      └─┘            └───┘    └──────────┘    
src                           └────┘   └─┘      └─┘             └───┘    └──────────┘
typ           └┘           └────┘   └─┘      └─┘            └───┘    └──────────┘    
doc                           └────┘            
487      suffices v ∘ f ⊗ t = (v ⊗ t) ∘ (inl ∘ f ⊗ inr), by simp [this],
id                              └─┘     └─┘            └──┘
src                                 └─┘     └─┘      └────┘    
typ                             └─┘     └─┘      └────┘└──┘
doc                                                      └────┘    
txt                                                         └────┘    
par                                                         └────┘    
pid                                                                 
st                                                         └──────────┘
488      funext $ λs, by cases s with a b; refl⟩
id       └────┘               
src      └────┘          └────┘ └───────┘  └──┘
typ      └────┘         └────┘└───────┘  └──┘
doc                      └────┘ └───────┘  └──┘
txt                      └────┘ └───────┘  └──┘
par                      └────┘ └───────┘  └──┘
pid                            └───────┘
st                      └─────────────────────┘
489  
490    theorem dioph_list_all (l) (d : list_all dioph l) : dioph (λv, list_all (λS : set (α → ℕ), S v) l) :=
id                                     └──────┘ └───┘     └───┘     └──────┘       └─┘           
src                                    └──────┘ └───┘      └───┘      └──────┘       └─┘      
typ                                    └──────┘ └───┘     └───┘     └──────┘       └─┘           
doc                                    └──────┘ └───┘      └───┘      └──────┘
491    suffices ∃ β (pl : list (poly (α ⊕ β))), ∀ v, list_all (λS : set _, S v) l ↔ ∃t, list_all (λp : poly (α ⊕ β), p (v ⊗ t) = 0) pl,
id                      └──┘  └──┘            └──────┘       └─┘          └──────┘       └──┘                 └┘
src                      └──┘  └──┘               └──────┘       └─┘              └──────┘       └──┘                  
typ                     └──┘  └──┘            └──────┘       └─┘          └──────┘       └──┘                 └┘
doc                             └──┘                 └──────┘                           └──────┘       └──┘               
492      from let ⟨β, pl, h⟩ := this in ⟨β, poly.sumsq pl, λv, (h v).trans $ exists_congr $ λt, (poly.sumsq_eq_zero _ _).symm⟩,
id            └─┘    └┘       └──┘        └────────┘            └───┘    └──────────┘       └────────────────┘     └──┘
src                                         └────────┘              └───┘    └──────────┘        └────────────────┘     └──┘
typ           └─┘    └┘       └──┘        └────────┘            └───┘    └──────────┘       └────────────────┘     └──┘
doc                                         └────────┘
493    begin
st     └─────
494      induction l with S l IH,
id                 
src      └────────┘ └──────────┘
typ      └────────┘└──────────┘
doc      └────────┘ └──────────┘
txt      └────────┘ └──────────┘
par      └────────┘ └──────────┘
pid                └─────────┘
st   ──────────────────────────┘└─
495      exact ⟨ulift empty, [], λv, by simp; exact ⟨λ⟨t⟩, empty.rec _ t, trivial⟩⟩,
id              └───┘ └───┘
src      └────┘ └───┘└───┘└┘  └┘ └─┘  └──┘└──────┘   └─┘         └─┘ └┘       └┘
typ      └────┘ └───┘└───┘└┘  └┘ └─┘  └──┘└──────┘   └─┘         └─┘ └┘       └┘
doc      └────┘ └───┘     └┘  └┘ └─┘  └──┘└──────┘   └─┘         └─┘ └┘       └┘
txt      └────┘           └┘  └┘ └─┘  └──┘└──────┘   └─┘         └─┘ └┘       └┘
par      └────┘           └┘  └┘ └─┘  └──┘└──────┘   └─┘         └─┘ └┘       └┘
pid                      └┘  └┘ └─┘  └───────────┘   └─┘         └─┘ └┘       └┘
st   ─────────────────────────────────┘└─────────────────────────────────────────┘└─
496      simp at d,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
pid          └──┘
st   ────────────┘└─
497      exact let ⟨⟨β, p, pe⟩, dl⟩ := d, ⟨γ, pl, ple⟩ := IH dl in
id                            └┘          └┘          └┘
src      └────┘      └┘ └┘  └─┘  └───┘ └┘  └┘  └┘   └───┘    └───
typ      └────┘     └┘└┘  └─┘└┘└───┘└┘ └┘└┘└┘   └───┘└┘  └───
doc      └────┘      └┘ └┘  └─┘  └───┘ └┘  └┘  └┘   └───┘    └───
txt      └────┘      └┘ └┘  └─┘  └───┘ └┘  └┘  └┘   └───┘    └───
par      └────┘      └┘ └┘  └─┘  └───┘ └┘  └┘  └┘   └───┘    └───
pid                 └┘ └┘  └─┘  └───┘ └┘  └┘  └┘   └───┘    └───
st   ──────────────────────────────────────────────────────────────
498      ⟨β ⊕ γ, p.remap (inl ⊗ inr ∘ inl) :: pl.map (λq, q.remap (inl ⊗ (inr ∘ inr))), λv,
id               └────┘                      └──┘       └────┘  └─┘          └─┘
src  ───┘   └┘ └────┘          └┘    └──┘  └─┘ └────┘ └─┘      └─┘└───┘ └──
typ  ───┘   └┘ └────┘          └┘    └──┘  └─┘ └────┘ └─┘      └─┘└───┘ └──
doc  ───┘    └┘ └────┘           └┘          └─┘ └────┘             └───┘ └──
txt  ───┘    └┘                   └┘          └─┘                    └───┘ └──
par  ───┘    └┘                   └┘          └─┘                    └───┘ └──
pid  ───┘    └┘                   └┘          └─┘                    └───┘ └──
st   ───────────────────────────────────────────────────────────────────────────────────────
499        by simp; exact iff.trans (and_congr (pe v) (ple v))
id                        └───────┘  └───────┘  └┘     └─┘ 
src  ─────┘  └──┘└──────┘└───────┘ └───────┘    └┘     └──
typ  ─────┘  └──┘└──────┘└───────┘ └───────┘ └┘ └┘ └─┘└──
doc  ─────┘  └──┘└──────┘                       └┘     └──
txt  ─────┘  └──┘└──────┘                       └┘     └──
par  ─────┘  └──┘└──────┘                       └┘     └──
pid  ─────┘  └───────────┘                       └┘     └──
st   ───────┘└─────────────────────────────────────────────────
500        ⟨λ⟨⟨m, hm⟩, ⟨n, hn⟩⟩,
id                     
src  ─────┘    └┘  └─┘  └┘  └───
typ  ─────┘   └┘  └─┘ └┘  └───
doc  ─────┘    └┘  └─┘  └┘  └───
txt  ─────┘    └┘  └─┘  └┘  └───
par  ─────┘    └┘  └─┘  └┘  └───
pid  ─────┘    └┘  └─┘  └┘  └───
st   ────────────────────────────
501          ⟨m ⊗ n, by rw [
src  ───────┘    └┘  └────
typ  ───────┘    └┘  └────
doc  ───────┘    └┘  └────
txt  ───────┘    └┘  └────
par  ───────┘    └┘  └────
pid  ───────┘    └┘  └─────
st   ─────────────────┘└─────
502            show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m,
id                                      └─┘   └─┘      
src  ─────────┘          └┘      └─┘ └─┘└┘   └─
typ  ─────────┘         └┘      └─┘ └─┘└┘ └─
doc  ─────────┘          └┘             └┘    └─
txt  ─────────┘          └┘             └┘    └─
par  ─────────┘          └┘             └┘    └─
pid  ─────────┘          └┘             └┘    └─
st   ────────────────────────────────────────────────────────
503            from funext $ λs, by cases s with a b; refl]; exact hm,
id                  └────┘                                        └┘
src  ──────────────┘└────┘  └─┘  └────┘ └───────┘└┘└──┘└──────┘  └─
typ  ──────────────┘└────┘  └─┘  └────┘└───────┘└┘└──┘└──────┘└┘└─
doc  ──────────────┘        └─┘  └────┘ └───────┘└┘└──┘└──────┘  └─
txt  ──────────────┘        └─┘  └────┘ └───────┘└┘└──┘└──────┘  └─
par  ──────────────┘        └─┘  └────┘ └───────┘└┘└──┘└──────┘  └─
pid  ──────────────┘        └─┘  └─────┘ └──────────────────────┘  └─
st   ─────────────────────────────┘└─────────────────────┘└────────┘└─
504          by { refine list_all.imp (λq hq, _) hn, dsimp [(∘)],
id                       └──────────┘            └┘         
src  ───────┘  └─┘└─────┘└──────────┘  └───────┘  └┘└─────┘└─┘└─
typ  ───────┘  └────────┘└──────────┘  └───────┘└┘└┘└─────┘└─┘└─
doc  ───────┘  └─┘└─────┘              └───────┘  └┘└─────┘ └─┘└─
txt  ───────┘  └─┘└─────┘              └───────┘  └┘└─────┘ └─┘└─
par  ───────┘  └────────┘              └───────┘  └┘└─────┘ └─┘└─
pid  ───────┘  └────────┘              └───────┘  └───────┘ └────
st   ─────────┘└──────────────────────────────────┘└───────────┘└─
505               rw [show (λ (x : α ⊕ γ), (v ⊗ m ⊗ n) ((inl ⊗ λ (x : γ), inr (inr x)) x)) = v ⊗ n,
id                                                    └─┘                  └─┘             
src  ────────────┘└──┘      └────┘   └─┘      └┘  └─┘  └────┘ └─┘    └─┘ └─┘ └─┘    └─
typ  ────────────┘└──┘      └────┘ └─┘     └┘  └─┘  └────┘└─┘    └─┘ └─┘ └─┘ └─
doc  ────────────┘└──┘      └────┘   └─┘      └┘       └────┘ └─┘        └─┘ └─┘    └─
txt  ────────────┘└──┘      └────┘   └─┘      └┘       └────┘ └─┘        └─┘ └─┘    └─
par  ────────────┘└──┘      └────┘   └─┘      └┘       └────┘ └─┘        └─┘ └─┘    └─
pid  ────────────────┘      └────┘   └─┘      └┘       └────┘ └─┘        └─┘ └─┘    └─
st   ───────────────────────────────────────────────────────────────────────────────────────────────
506                   from funext $ λs, by cases s with a b; refl]; exact hq }⟩,
id                         └────┘                                        └┘
src  ─────────────────────┘└────┘  └─┘  └────┘ └───────┘└┘└──┘└──────┘  └────
typ  ─────────────────────┘└────┘  └─┘  └────┘└───────┘└┘└──┘└──────┘└┘└────
doc  ─────────────────────┘        └─┘  └────┘ └───────┘└┘└──┘└──────┘  └────
txt  ─────────────────────┘        └─┘  └────┘ └───────┘└┘└──┘└──────┘  └────
par  ─────────────────────┘        └─┘  └────┘ └───────┘└┘└──┘└──────┘  └────
pid  ─────────────────────┘        └─┘  └─────┘ └──────────────────────┘  └────
st   ────────────────────────────────────┘└─────────────────────┘└─────────┘└──
507        λ⟨t, hl, hr⟩,
id           
src  ─────┘  └┘  └┘  └──
typ  ─────┘ └┘  └┘  └──
doc  ─────┘  └┘  └┘  └──
txt  ─────┘  └┘  └┘  └──
par  ─────┘  └┘  └┘  └──
pid  ─────┘  └┘  └┘  └──
st   ────────────────────
508          ⟨⟨t ∘ inl, by rwa [
src  ───────┘       └┘  └─────
typ  ───────┘       └┘  └─────
doc  ───────┘       └┘  └─────
txt  ───────┘       └┘  └─────
par  ───────┘       └┘  └─────
pid  ───────┘       └┘  └──────
st   ────────────────────┘└──────
509            show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl,
id                                   └─┘               └─┘
src  ─────────┘        └┘      └─┘    └┘     └─┘└─
typ  ─────────┘        └┘      └─┘    └┘  └─┘└─
doc  ─────────┘        └┘             └┘        └─
txt  ─────────┘        └┘             └┘        └─
par  ─────────┘        └┘             └┘        └─
pid  ─────────┘        └┘             └┘        └─
st   ──────────────────────────────────────────────────────────
510            from funext $ λs, by cases s with a b; refl] at hl⟩,
id                  └────┘                
src  ──────────────┘└────┘  └─┘  └────┘ └───────┘└┘└──┘└─────┘└──
typ  ──────────────┘└────┘  └─┘  └────┘└───────┘└┘└──┘└─────┘└──
doc  ──────────────┘        └─┘  └────┘ └───────┘└┘└──┘└─────┘└──
txt  ──────────────┘        └─┘  └────┘ └───────┘└┘└──┘└─────┘└──
par  ──────────────┘        └─┘  └────┘ └───────┘└┘└──┘└─────┘└──
pid  ──────────────┘        └─┘  └─────┘ └────────────────────────
st   ─────────────────────────────┘└─────────────────────┘└────┘└──
511          ⟨t ∘ inr, by {
src  ───────┘      └┘  └──
typ  ───────┘      └┘  └──
doc  ───────┘      └┘  └──
txt  ───────┘      └┘  └──
par  ───────┘      └┘  └──
pid  ───────┘      └┘  └──
st   ───────────────────┘└──
512            refine list_all.imp (λq hq, _) hr, dsimp [(∘)] at hq,
id                    └──────────┘            └┘         
src  ─────────┘└─────┘└──────────┘  └───────┘  └┘└─────┘└───────┘└─
typ  ────────────────┘└──────────┘  └───────┘└┘└┘└─────┘└───────┘└─
doc  ─────────┘└─────┘              └───────┘  └┘└─────┘ └───────┘└─
txt  ─────────┘└─────┘              └───────┘  └┘└─────┘ └───────┘└─
par  ────────────────┘              └───────┘  └┘└─────┘ └───────┘└─
pid  ────────────────┘              └───────┘  └───────┘ └──────────
st   ──────────────────────────────────────────┘└─────────────────┘└─
513            rwa [show (λ (x : α ⊕ γ), (v ⊗ t) ((inl ⊗ λ (x : γ), inr (inr x)) x)) = v ⊗ t ∘ inr,
id                                                └─┘                                     └─┘
src  ─────────┘└───┘      └────┘   └─┘    └┘  └─┘  └────┘ └─┘        └─┘ └─┘     └─┘└─
typ  ─────────┘└───┘      └────┘  └─┘    └┘  └─┘  └────┘└─┘        └─┘ └─┘  └─┘└─
doc  ─────────┘└───┘      └────┘   └─┘    └┘       └────┘ └─┘        └─┘ └─┘        └─
txt  ─────────┘└───┘      └────┘   └─┘    └┘       └────┘ └─┘        └─┘ └─┘        └─
par  ─────────┘└───┘      └────┘   └─┘    └┘       └────┘ └─┘        └─┘ └─┘        └─
pid  ──────────────┘      └────┘   └─┘    └┘       └────┘ └─┘        └─┘ └─┘        └─
st   ───────────────────────────────────────────────────────────────────────────────────────────────
514                 from funext $ λs, by cases s with a b; refl] at hq }⟩⟩⟩⟩
id                       └────┘                
src  ───────────────────┘└────┘  └─┘  └────┘ └───────┘└┘└──┘└──────┘└─────
typ  ───────────────────┘└────┘  └─┘  └────┘└───────┘└┘└──┘└──────┘└─────
doc  ───────────────────┘        └─┘  └────┘ └───────┘└┘└──┘└──────┘└─────
txt  ───────────────────┘        └─┘  └────┘ └───────┘└┘└──┘└──────┘└─────
par  ───────────────────┘        └─┘  └────┘ └───────┘└┘└──┘└──────┘└─────
pid  ───────────────────┘        └─┘  └─────┘ └──────────────────────────┘
st   ──────────────────────────────────┘└─────────────────────┘└─────┘└─┘└─
515    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
516  
517    theorem and_dioph {S S' : set (α → ℕ)} (d : dioph S) (d' : dioph S') : dioph (λv, S v ∧ S' v) :=
id                               └─┘             └───┘         └───┘ └┘    └───┘        └┘ 
src                              └─┘              └───┘          └───┘       └───┘          
typ                              └─┘             └───┘         └───┘ └┘    └───┘        └┘ 
doc                                                └───┘          └───┘       └───┘
518    dioph_list_all [S, S'] ⟨d, d'⟩
id     └────────────┘  └┘    └┘
src    └────────────┘     
typ    └────────────┘  └┘    └┘
519  
520    theorem or_dioph {S S' : set (α → ℕ)} : ∀ (d : dioph S) (d' : dioph S'), dioph (λv, S v ∨ S' v)
id                              └─┘                └───┘         └───┘ └┘   └───┘        └┘ 
src                             └─┘                  └───┘          └───┘      └───┘          
typ                             └─┘                └───┘         └───┘ └┘   └───┘        └┘ 
doc                                                   └───┘          └───┘      └───┘
521    | ⟨β, p, pe⟩ ⟨γ, q, qe⟩ := ⟨β ⊕ γ, p.remap (inl ⊗ inr ∘ inl) * q.remap (inl ⊗ inr ∘ inr), λv,
id                                    └────┘  └─┘  └─┘  └─┘    └────┘  └─┘  └─┘  └─┘    
src                                       └────┘  └─┘  └─┘  └─┘    └────┘  └─┘  └─┘  └─┘
typ                                   └────┘  └─┘  └─┘  └─┘    └────┘  └─┘  └─┘  └─┘    
doc                                        └────┘                     └────┘      
522      begin
st       └─────
523        refine iff.trans (or_congr ((pe v).trans _) ((qe v).trans _)) (exists_or_distrib.symm.trans (exists_congr $ λt,
id                └───────┘  └──────┘   └┘               └┘               └──────────────────────────┘  └──────────┘
src        └─────┘└───────┘ └──────┘     └─────────┘     └──────────┘ └──────────────────────────┘ └──────────┘  └──
typ        └─────┘└───────┘ └──────┘  └┘ └─────────┘  └┘ └──────────┘ └──────────────────────────┘ └──────────┘  └──
doc        └─────┘                       └─────────┘     └──────────┘                                            └──
txt        └─────┘                       └─────────┘     └──────────┘                                            └──
par        └─────┘                       └─────────┘     └──────────┘                                            └──
pid                                     └─────────┘     └──────────┘                                            └──
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
524         (@mul_eq_zero_iff_eq_zero_or_eq_zero _ _ (p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl))) (q ((v ⊗ t) ∘ (inl ⊗ inr ∘ inr)))).symm)),
id            └────────────────────────────────┘                                                 └─┘         └─┘
src  ──────┘  └────────────────────────────────┘└───┘      └┘            └──┘       └┘  └─┘     └─┘└─────────┘
typ  ──────┘  └────────────────────────────────┘└───┘     └┘            └──┘     └┘  └─┘     └─┘└─────────┘
doc  ──────┘                                    └───┘      └┘             └──┘       └┘             └─────────┘
txt  ──────┘                                    └───┘       └┘             └──┘       └┘             └─────────┘
par  ──────┘                                    └───┘       └┘             └──┘       └┘             └─────────┘
pid  ──────┘                                    └───┘       └┘             └──┘       └┘             └─────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
525        exact inject_dummies_lem _ (some ⊗ (λ_, none)) (λx, rfl) _ _,
id               └────────────────┘    └──┘        └──┘        └─┘
src        └────┘└────────────────┘└─┘ └──┘   └─┘└──┘└─┘  └─┘└─┘└───┘
typ        └────┘└────────────────┘└─┘ └──┘   └─┘└──┘└─┘  └─┘└─┘└───┘
doc        └────┘                  └─┘        └─┘    └─┘  └─┘   └───┘
txt        └────┘                  └─┘        └─┘    └─┘  └─┘   └───┘
par        └────┘                  └─┘        └─┘    └─┘  └─┘   └───┘
pid                               └─┘        └─┘    └─┘  └─┘   └───┘
st   ─────────────────────────────────────────────────────────────────┘└─
526        exact inject_dummies_lem _ ((λ_, none) ⊗ some) (λx, rfl) _ _,
id               └────────────────┘         └──┘    └──┘       └─┘
src        └────┘└────────────────┘└─┘   └─┘└──┘└┘ └──┘└┘  └─┘└─┘└───┘
typ        └────┘└────────────────┘└─┘   └─┘└──┘└┘ └──┘└┘  └─┘└─┘└───┘
doc        └────┘                  └─┘   └─┘    └┘     └┘  └─┘   └───┘
txt        └────┘                  └─┘   └─┘    └┘     └┘  └─┘   └───┘
par        └────┘                  └─┘   └─┘    └┘     └┘  └─┘   └───┘
pid                               └─┘   └─┘    └┘     └┘  └─┘   └───┘
st   ─────────────────────────────────────────────────────────────────┘└─
527      end⟩
st   ──────┘
528  
529    /-- A partial function is Diophantine if its graph is Diophantine. -/
530    def dioph_pfun (f : (α → ℕ) →. ℕ) := dioph (λv : option α → ℕ, f.graph (v ∘ some, v none))
id                               └┘      └───┘       └────┘     └────┘   └──┘   └──┘
src                               └┘      └───┘       └────┘        └────┘    └──┘    └──┘
typ                              └┘      └───┘       └────┘     └────┘   └──┘   └──┘
doc                                └┘       └───┘                      └────┘
531  
532    /-- A function is Diophantine if its graph is Diophantine. -/
533    def dioph_fn (f : (α → ℕ) → ℕ) := dioph (λv : option α → ℕ, f (v ∘ some) = v none)
id                                   └───┘       └────┘         └──┘    └──┘
src                                    └───┘       └────┘             └──┘     └──┘
typ                                  └───┘       └────┘         └──┘    └──┘
doc                                      └───┘
534  
535    theorem reindex_dioph_fn {f : (α → ℕ) → ℕ} (d : dioph_fn f) (g : α → β) : dioph_fn (λv, f (v ∘ g)) :=
id                                                 └──────┘               └──────┘         
src                                                  └──────┘                  └──────┘           
typ                                                └──────┘               └──────┘         
doc                                                    └──────┘                  └──────┘
536    reindex_dioph d (functor.map g)
id     └───────────┘   └─────────┘ 
src    └───────────┘    └─────────┘
typ    └───────────┘   └─────────┘ 
537  
538    theorem ex_dioph {S : set (α ⊕ β → ℕ)} : dioph S → dioph (λv, ∃x, S (v ⊗ x))
id                           └─┘            └───┘   └───┘          
src                          └─┘              └───┘     └───┘             
typ                          └─┘            └───┘   └───┘          
doc                                             └───┘     └───┘               
539    | ⟨γ, p, pe⟩ := ⟨β ⊕ γ, p.remap ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr), λv,
id            └┘            └────┘   └─┘  └─┘  └─┘   └─┘  └─┘    
src                            └────┘   └─┘  └─┘  └─┘   └─┘  └─┘
typ           └┘            └────┘   └─┘  └─┘  └─┘   └─┘  └─┘    
doc                             └────┘                   
540      ⟨λ⟨x, hx⟩, let ⟨t, ht⟩ := (pe _).1 hx in ⟨x ⊗ t, by simp; rw [
id           └┘   └─┘                            
src                                                        └──┘  └────
typ          └┘   └─┘                                   └──┘  └────
doc                                                         └──┘  └────
txt                                                          └──┘  └────
par                                                          └──┘  └────
pid                                                                  └──
st                                                          └─────────┘
541        show (v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) = (v ⊗ x) ⊗ t,
id                                        └─┘          └─┘           
src  ─────┘         └┘          └─┘└┘     └─┘└┘    └┘  └─
typ  ─────┘         └┘          └─┘└┘     └─┘└┘  └┘ └─
doc  ─────┘         └┘              └┘        └┘     └┘  └─
txt  ─────┘          └┘              └┘        └┘     └┘  └─
par  ─────┘          └┘              └┘        └┘     └┘  └─
pid  ─────┘          └┘              └┘        └┘     └┘  └─
st   ────────────────────────────────────────────────────────────────────────
542        from funext $ λs, by cases s with a b; try {cases a}; refl]; exact ht⟩,
id              └────┘                                                      └┘
src  ──────────┘└────┘  └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘  └────┘
typ  ──────────┘└────┘  └─┘  └────┘└───────┘└┘└───┘└────┘└┘└──┘  └────┘└┘
doc  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘  └────┘
txt  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘  └────┘
par  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘  └────┘
pid  ──────────┘        └─┘  └─────┘ └────────────────────┘ └──────┘       
st   ─────────────────────────┘└──────────────────────┘└─────┘└────┘└────────┘
543      λ⟨t, ht⟩, ⟨t ∘ inl, (pe _).2 ⟨t ∘ inr, by simp at ht; rwa [
id                   └─┘              └─┘
src                    └─┘              └─┘     └────────┘  └─────
typ                  └─┘              └─┘     └────────┘  └─────
doc                                                └────────┘  └─────
txt                                                └────────┘  └─────
par                                                └────────┘  └─────
pid                                                    └───┘     └──
st                                                └────────────────┘
544        show (v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) = (v ⊗ t ∘ inl) ⊗ t ∘ inr,
id                                                                 └─┘       └─┘
src  ─────┘        └┘              └┘        └┘      └─┘└┘   └─┘└─
typ  ─────┘        └┘              └┘        └┘    └─┘└┘  └─┘└─
doc  ─────┘        └┘              └┘        └┘         └┘      └─
txt  ─────┘        └┘              └┘        └┘         └┘      └─
par  ─────┘        └┘              └┘        └┘         └┘      └─
pid  ─────┘        └┘              └┘        └┘         └┘      └─
st   ────────────────────────────────────────────────────────────────────────────────
545        from funext $ λs, by cases s with a b; try {cases a}; refl] at ht⟩⟩⟩⟩
id              └────┘                                      
src  ──────────┘└────┘  └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘└─────┘
typ  ──────────┘└────┘  └─┘  └────┘└───────┘└┘└───┘└────┘└┘└──┘└─────┘
doc  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘└─────┘
txt  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘└─────┘
par  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘└─────┘
pid  ──────────┘        └─┘  └─────┘ └────────────────────┘ └──────┘└────┘
st   ─────────────────────────┘└──────────────────────┘└─────┘└────┘└────┘
546  
547    theorem ex1_dioph {S : set (option α → ℕ)} : dioph S → dioph (λv, ∃x, S (x :: v))
id                            └─┘  └────┘         └───┘   └───┘         └┘ 
src                           └─┘  └────┘          └───┘     └───┘             └┘
typ                           └─┘  └────┘         └───┘   └───┘         └┘ 
doc                                                 └───┘     └───┘               └┘
548    | ⟨β, p, pe⟩ := ⟨option β, p.remap (inr none :: inl ⊗ inr ∘ some), λv,
id            └┘      └────┘     └────┘  └─┘ └──┘ └┘ └─┘  └─┘  └──┘    
src                     └────┘     └────┘  └─┘ └──┘ └┘ └─┘  └─┘  └──┘
typ           └┘      └────┘     └────┘  └─┘ └──┘ └┘ └─┘  └─┘  └──┘    
doc                                └────┘           └┘     
549      ⟨λ⟨x, hx⟩, let ⟨t, ht⟩ := (pe _).1 hx in ⟨x :: t, by simp; rw [
id           └┘   └─┘                            └┘
src                                                 └┘       └──┘  └────
typ          └┘   └─┘                            └┘       └──┘  └────
doc                                                  └┘       └──┘  └────
txt                                                           └──┘  └────
par                                                           └──┘  └────
pid                                                                   └──
st                                                           └─────────┘
550        show (v ⊗ x :: t) ∘ (inr none :: inl ⊗ inr ∘ some) = x :: v ⊗ t,
id                    └┘          └──┘    └─┘   └─┘   └──┘          
src  ─────┘       └┘ └┘    └──┘  └─┘ └─┘ └──┘└┘      └─
typ  ─────┘       └┘ └┘    └──┘  └─┘ └─┘ └──┘└┘   └─
doc  ─────┘       └┘ └┘                       └┘       └─
txt  ─────┘           └┘                       └┘       └─
par  ─────┘           └┘                       └┘       └─
pid  ─────┘           └┘                       └┘       └─
st   ───────────────────────────────────────────────────────────────────────
551        from funext $ λs, by cases s with a b; try {cases a}; refl]; exact ht⟩,
id              └────┘                                                      └┘
src  ──────────┘└────┘  └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘  └────┘
typ  ──────────┘└────┘  └─┘  └────┘└───────┘└┘└───┘└────┘└┘└──┘  └────┘└┘
doc  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘  └────┘
txt  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘  └────┘
par  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘  └────┘
pid  ──────────┘        └─┘  └─────┘ └────────────────────┘ └──────┘       
st   ─────────────────────────┘└──────────────────────┘└─────┘└────┘└────────┘
552      λ⟨t, ht⟩, ⟨t none, (pe _).2 ⟨t ∘ some, by simp at ht; rwa [
id                  └──┘              └──┘
src                   └──┘              └──┘     └────────┘  └─────
typ                 └──┘              └──┘     └────────┘  └─────
doc                                                └────────┘  └─────
txt                                                └────────┘  └─────
par                                                └────────┘  └─────
pid                                                    └───┘     └──
st                                                └────────────────┘
553        show (v ⊗ t) ∘ (inr none :: inl ⊗ inr ∘ some) = t none :: v ⊗ t ∘ some,
id                                     └─┘   └─┘            └──┘          └──┘
src  ─────┘        └┘           └─┘ └─┘     └┘  └──┘      └──┘└─
typ  ─────┘        └┘           └─┘ └─┘     └┘ └──┘    └──┘└─
doc  ─────┘        └┘                       └┘                └─
txt  ─────┘        └┘                       └┘                └─
par  ─────┘        └┘                       └┘                └─
pid  ─────┘        └┘                       └┘                └─
st   ──────────────────────────────────────────────────────────────────────────────
554        from funext $ λs, by cases s with a b; try {cases a}; refl] at ht⟩⟩⟩⟩
id              └────┘                                      
src  ──────────┘└────┘  └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘└─────┘
typ  ──────────┘└────┘  └─┘  └────┘└───────┘└┘└───┘└────┘└┘└──┘└─────┘
doc  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘└─────┘
txt  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘└─────┘
par  ──────────┘        └─┘  └────┘ └───────┘└┘└───┘└────┘ └┘└──┘└─────┘
pid  ──────────┘        └─┘  └─────┘ └────────────────────┘ └──────┘└────┘
st   ─────────────────────────┘└──────────────────────┘└─────┘└────┘└────┘
555  
556    theorem dom_dioph {f : (α → ℕ) →. ℕ} (d : dioph_pfun f) : dioph f.dom :=
id                                  └┘        └────────┘     └───┘ └──┘
src                                  └┘        └────────┘      └───┘  └──┘
typ                                 └┘        └────────┘     └───┘ └──┘
doc                                   └┘         └────────┘      └───┘  └──┘
557    cast (congr_arg dioph $ set.ext $ λv, (pfun.dom_iff_graph _ _).symm) (ex1_dioph d)
id     └──┘  └───────┘ └───┘   └─────┘       └────────────────┘     └──┘    └───────┘ 
src    └──┘  └───────┘ └───┘   └─────┘        └────────────────┘     └──┘    └───────┘
typ    └──┘  └───────┘ └───┘   └─────┘       └────────────────┘     └──┘    └───────┘ 
doc                    └───┘
558  
559    theorem dioph_fn_iff_pfun (f : (α → ℕ) → ℕ) : dioph_fn f = @dioph_pfun α f :=
id                                               └──────┘    └────────┘  
src                                                └──────┘     └────────┘
typ                                              └──────┘    └────────┘  
doc                                                  └──────┘      └────────┘
560    by refine congr_arg dioph (set.ext $ λv, _); exact pfun.lift_graph.symm
id               └───────┘ └───┘  └─────┘                 └──────────────────┘
src       └─────┘└───────┘└───┘ └─────┘  └───┘  └────┘└──────────────────┘
typ       └─────┘└───────┘└───┘ └─────┘  └───┘  └────┘└──────────────────┘
doc       └─────┘         └───┘          └───┘  └────┘                    
txt       └─────┘                        └───┘  └────┘                    
par       └─────┘                        └───┘  └────┘                    
pid                                     └───┘                           
st       └─────────────────────────────────────────────────────────────────────
561  
src  
typ  
doc  
txt  
par  
pid  
st   
562    theorem abs_poly_dioph (p : poly α) : dioph_fn (λv, (p v).nat_abs) :=
id                                 └──┘     └──────┘        └─────┘
src  ─┘                            └──┘      └──────┘           └─────┘
typ  ─┘                            └──┘     └──────┘        └─────┘
doc  ─┘                            └──┘      └──────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
563    by refine of_no_dummies _ ((p.remap some - poly.proj none) * (p.remap some + poly.proj none)) (λv, _);
id               └───────────┘                                     └─────┘ └──┘  └───────┘ └──┘
src       └─────┘└───────────┘└─┘                          └┘ └─────┘└──┘└───────┘└──┘└─┘  └───┘
typ       └─────┘└───────────┘└─┘                          └┘ └─────┘└──┘└───────┘└──┘└─┘  └───┘
doc       └─────┘             └─┘                           └┘  └─────┘     └───────┘    └─┘  └───┘
txt       └─────┘             └─┘                           └┘                           └─┘  └───┘
par       └─────┘             └─┘                           └┘                           └─┘  └───┘
pid                          └─┘                           └┘                           └─┘  └───┘
st       └────────────────────────────────────────────────────────────────────────────────────────────────────
564       apply int.eq_nat_abs_iff_mul
id              └────────────────────┘
src       └────┘└────────────────────┘
typ       └────┘└────────────────────┘
doc       └────┘                      
txt       └────┘                      
par       └────┘                      
pid                                  
st   ──────────────────────────────────
565  
src  
typ  
doc  
txt  
par  
pid  
st   
566    theorem proj_dioph (i : α) : dioph_fn (λv, v i) :=
id                                 └──────┘      
src  ─┘                             └──────┘
typ  ─┘                            └──────┘      
doc  ─┘                             └──────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
567    abs_poly_dioph (poly.proj i)
id     └────────────┘  └───────┘ 
src    └────────────┘  └───────┘
typ    └────────────┘  └───────┘ 
doc                    └───────┘
568  
569    theorem dioph_pfun_comp1 {S : set (option α → ℕ)} (d : dioph S) {f} (df : dioph_pfun f) :
id                                   └─┘  └────┘            └───┘             └────────┘ 
src                                  └─┘  └────┘             └───┘              └────────┘
typ                                  └─┘  └────┘            └───┘             └────────┘ 
doc                                                           └───┘              └────────┘
570      dioph (λv : α → ℕ, ∃ h : f.dom v, S (f.fn v h :: v)) :=
id       └───┘                └──┘    └─┘   └┘ 
src      └───┘                   └──┘       └─┘     └┘
typ      └───┘                └──┘    └─┘   └┘ 
doc      └───┘                     └──┘        └─┘     └┘
571    ext (ex1_dioph (and_dioph d df)) $ λv,
id     └─┘  └───────┘  └───────┘  └┘      
src    └─┘  └───────┘  └───────┘
typ    └─┘  └───────┘  └───────┘  └┘      
572    ⟨λ⟨x, hS, (h: Exists _)⟩, by
id                  └────┘
src                  └────┘
typ                 └────┘
st                                 
573      rw [show (x :: v) ∘ some = v, from funext $ λs, rfl] at h;
id                  └┘     └──┘         └────┘       └─┘
src      └──┘      └┘ └┘└──┘ └─────┘└────┘  └─┘└─┘└────┘
typ      └──┘     └┘ └┘└──┘└─────┘└────┘  └─┘└─┘└────┘
doc      └──┘      └┘ └┘       └─────┘        └─┘   └────┘
txt      └──┘         └┘       └─────┘        └─┘   └────┘
par      └──┘         └┘       └─────┘        └─┘   └────┘
pid        └┘         └┘       └─────┘        └─┘   └───┘
st   ──────────────────────────────────────────────────────┘└──────
574      cases h with hf h; refine ⟨hf, _⟩; rw [pfun.fn, h]; exact hS,
id                                 └┘          └─────┘           └┘
src      └────┘ └────────┘  └─────┘   └──┘  └──┘└─────┘└┘   └────┘
typ      └────┘└────────┘  └─────┘ └┘└──┘  └──┘└─────┘└┘  └────┘└┘
doc      └────┘ └────────┘  └─────┘   └──┘  └──┘└─────┘└┘   └────┘
txt      └────┘ └────────┘  └─────┘   └──┘  └──┘       └┘   └────┘
par      └────┘ └────────┘  └─────┘   └──┘  └──┘       └┘   └────┘
pid            └────────┘           └──┘    └┘       └┘        
st   ──────────────────────────────────────────┘└─────┘└─┘└────────┘
575    λ⟨x, hS⟩, ⟨f.fn v x, hS, show Exists _,
id        └┘    └─┘              └────┘
src                └─┘               └────┘
typ       └┘    └─┘              └────┘
doc                └─┘
576      by rw [show (f.fn v x :: v) ∘ some = v, from funext $ λs, rfl]; exact ⟨x, rfl⟩⟩⟩
id                    └──┘            └──┘         └────┘       └─┘            └─┘
src         └──┘     └──┘     └┘ └──┘  └─────┘└────┘  └─┘└─┘  └────┘  └┘└─┘
typ         └──┘     └──┘    └┘ └──┘└─────┘└────┘  └─┘└─┘  └────┘ └┘└─┘
doc         └──┘     └──┘     └┘       └─────┘        └─┘     └────┘  └┘   
txt         └──┘              └┘       └─────┘        └─┘     └────┘  └┘   
par         └──┘              └┘       └─────┘        └─┘     └────┘  └┘   
pid           └┘              └┘       └─────┘        └─┘            └┘   
st         └─────────────────────────────────────────────────────────┘└──────────────┘
577  
578    theorem dioph_fn_comp1 {S : set (option α → ℕ)} (d : dioph S) {f : (α → ℕ) → ℕ} (df : dioph_fn f) :
id                                 └─┘  └────┘            └───┘                       └──────┘ 
src                                └─┘  └────┘             └───┘                          └──────┘
typ                                └─┘  └────┘            └───┘                       └──────┘ 
doc                                                         └───┘                            └──────┘
579      dioph (λv : α → ℕ, S (f v :: v)) :=
id       └───┘               └┘ 
src      └───┘                    └┘
typ      └───┘               └┘ 
doc      └───┘                     └┘
580    ext (dioph_pfun_comp1 d (cast (dioph_fn_iff_pfun f) df)) $ λv,
id     └─┘  └──────────────┘   └──┘  └───────────────┘   └┘      
src    └─┘  └──────────────┘    └──┘  └───────────────┘
typ    └─┘  └──────────────┘   └──┘  └───────────────┘   └┘      
581    ⟨λ⟨_, h⟩, h, λh, ⟨trivial, h⟩⟩
id                    └─────┘  
src                      └─────┘
typ                   └─────┘  
582  
583  end
584  
585  section
586    variables {α β γ : Type}
id               
typ              
587    open vector3
588    open_locale vector3
589    theorem dioph_fn_vec_comp1 {n} {S : set (vector3 ℕ (succ n))} (d : dioph S) {f : (vector3 ℕ n) → ℕ} (df : dioph_fn f) :
id                                         └─┘  └─────┘   └──┘          └───┘         └─────┘              └──────┘ 
src                                        └─┘  └─────┘   └──┘           └───┘          └─────┘               └──────┘
typ                                        └─┘  └─────┘   └──┘          └───┘         └─────┘              └──────┘ 
doc                                             └─────┘                   └───┘          └─────┘                 └──────┘
590      dioph (λv : vector3 ℕ n, S (cons (f v) v)) :=
id       └───┘       └─────┘      └──┘     
src      └───┘       └─────┘        └──┘
typ      └───┘       └─────┘      └──┘     
doc      └───┘       └─────┘         └──┘
591    ext (dioph_fn_comp1 (reindex_dioph d (none :: some)) df) $ λv, by rw [
id     └─┘  └────────────┘  └───────────┘   └──┘ └┘ └──┘   └┘     
src    └─┘  └────────────┘  └───────────┘    └──┘ └┘ └──┘                └────
typ    └─┘  └────────────┘  └───────────┘   └──┘ └┘ └──┘   └┘          └────
doc                                               └┘                     └────
txt                                                                      └────
par                                                                      └────
pid                                                                        └──
st                                                                      └─────
592      show option.cons (f v) v ∘ (cons none some) = f v :: v,
id            └─────────┘           └──┘ └──┘ └──┘         
src  ───┘    └─────────┘   └┘  └──┘└──┘└──┘└┘     └─
typ  ───┘    └─────────┘   └┘  └──┘└──┘└──┘└┘   └─
doc  ───┘    └─────────┘   └┘   └──┘        └┘      └─
txt  ───┘                  └┘               └┘      └─
par  ───┘                  └┘               └┘      └─
pid  ───┘                  └┘               └┘      └─
st   ────────────────────────────────────────────────────────────
593      from funext $ λs, by cases s with a b; refl]
id            └────┘                
src  ────────┘└────┘  └─┘  └────┘ └───────┘└┘└──┘└─
typ  ────────┘└────┘  └─┘  └────┘└───────┘└┘└──┘└─
doc  ────────┘        └─┘  └────┘ └───────┘└┘└──┘└─
txt  ────────┘        └─┘  └────┘ └───────┘└┘└──┘└─
par  ────────┘        └─┘  └────┘ └───────┘└┘└──┘└─
pid  ────────┘        └─┘  └─────┘ └──────────────┘
st   ───────────────────────┘└─────────────────────┘
594  
src  
typ  
doc  
txt  
par  
pid  
st   
595    theorem vec_ex1_dioph (n) {S : set (vector3 ℕ (succ n))} (d : dioph S) : dioph (λv : vector3 ℕ n, ∃x, S (x :: v)) :=
id                                    └─┘  └─────┘   └──┘          └───┘     └───┘       └─────┘        └┘ 
src  ─┘                               └─┘  └─────┘   └──┘           └───┘      └───┘       └─────┘            └┘
typ  ─┘                               └─┘  └─────┘   └──┘          └───┘     └───┘       └─────┘        └┘ 
doc  ─┘                                    └─────┘                   └───┘      └───┘       └─────┘               └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
596    ext (ex1_dioph $ reindex_dioph d (none :: some)) $ λv, exists_congr $ λx, by rw [
id     └─┘  └───────┘   └───────────┘   └──┘ └┘ └──┘        └──────────┘    
src    └─┘  └───────┘   └───────────┘    └──┘ └┘ └──┘         └──────────┘          └────
typ    └─┘  └───────┘   └───────────┘   └──┘ └┘ └──┘        └──────────┘         └────
doc                                           └┘                                    └────
txt                                                                                 └────
par                                                                                 └────
pid                                                                                   └──
st                                                                                 └─────
597      show (option.cons x v) ∘ (cons none some) = x :: v,
id             └─────────┘        └──┘ └──┘ └──┘       
src  ───┘     └─────────┘  └┘ └──┘└──┘└──┘└┘    └─
typ  ───┘     └─────────┘  └┘ └──┘└──┘└──┘└┘  └─
doc  ───┘     └─────────┘  └┘  └──┘        └┘     └─
txt  ───┘                  └┘              └┘     └─
par  ───┘                  └┘              └┘     └─
pid  ───┘                  └┘              └┘     └─
st   ────────────────────────────────────────────────────────
598      from funext $ λs, by cases s with a b; refl]
id            └────┘                
src  ────────┘└────┘  └─┘  └────┘ └───────┘└┘└──┘└─
typ  ────────┘└────┘  └─┘  └────┘└───────┘└┘└──┘└─
doc  ────────┘        └─┘  └────┘ └───────┘└┘└──┘└─
txt  ────────┘        └─┘  └────┘ └───────┘└┘└──┘└─
par  ────────┘        └─┘  └────┘ └───────┘└┘└──┘└─
pid  ────────┘        └─┘  └─────┘ └──────────────┘
st   ───────────────────────┘└─────────────────────┘
599  
src  
typ  
doc  
txt  
par  
pid  
st   
600    theorem dioph_fn_vec {n} (f : vector3 ℕ n → ℕ) : dioph_fn f ↔ dioph (λv : vector3 ℕ (succ n), f (v ∘ fs) = v fz) :=
id                                   └─────┘         └──────┘   └───┘       └─────┘   └──┘        └┘    └┘
src  ─┘                              └─────┘          └──────┘    └───┘       └─────┘   └──┘           └┘     └┘
typ  ─┘                              └─────┘         └──────┘   └───┘       └─────┘   └──┘        └┘    └┘
doc  ─┘                              └─────┘            └──────┘     └───┘       └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
601    ⟨λh, reindex_dioph h (fz :: fs), λh, reindex_dioph h (none :: some)⟩
id         └───────────┘   └┘ └┘ └┘      └───────────┘   └──┘ └┘ └──┘
src         └───────────┘    └┘ └┘ └┘       └───────────┘    └──┘ └┘ └──┘
typ        └───────────┘   └┘ └┘ └┘      └───────────┘   └──┘ └┘ └──┘
doc                             └┘                                └┘
602  
603    theorem dioph_pfun_vec {n} (f : vector3 ℕ n →. ℕ) : dioph_pfun f ↔ dioph (λv : vector3 ℕ (succ n), f.graph (v ∘ fs, v fz)) :=
id                                     └─────┘   └┘     └────────┘   └───┘       └─────┘   └──┘    └────┘   └┘   └┘
src                                    └─────┘    └┘     └────────┘    └───┘       └─────┘   └──┘      └────┘    └┘    └┘
typ                                    └─────┘   └┘     └────────┘   └───┘       └─────┘   └──┘    └────┘   └┘   └┘
doc                                    └─────┘     └┘      └────────┘     └───┘       └─────┘              └────┘
604    ⟨λh, reindex_dioph h (fz :: fs), λh, reindex_dioph h (none :: some)⟩
id         └───────────┘   └┘ └┘ └┘      └───────────┘   └──┘ └┘ └──┘
src         └───────────┘    └┘ └┘ └┘       └───────────┘    └──┘ └┘ └──┘
typ        └───────────┘   └┘ └┘ └┘      └───────────┘   └──┘ └┘ └──┘
doc                             └┘                                └┘
605  
606    theorem dioph_fn_compn {α : Type} : ∀ {n} {S : set (α ⊕ fin2 n → ℕ)} (d : dioph S) {f : vector3 ((α → ℕ) → ℕ) n} (df : vector_allp dioph_fn f),
id                                                  └─┘    └──┘            └───┘        └─────┘                   └─────────┘ └──────┘ 
src                                                   └─┘     └──┘             └───┘         └─────┘                      └─────────┘ └──────┘
typ                                                 └─┘    └──┘            └───┘        └─────┘                   └─────────┘ └──────┘ 
doc                                                            └──┘              └───┘         └─────┘                        └─────────┘ └──────┘
607      dioph (λv : α → ℕ, S (v ⊗ λi, f i v))
id       └───┘                    
src      └───┘                  
typ      └───┘                    
doc      └───┘                   
608    | 0 S d f := λdf, ext (reindex_dioph d (id ⊗ fin2.elim0)) $ λv,
id                  └┘  └─┘  └───────────┘    └┘  └────────┘      
src                      └─┘  └───────────┘    └┘  └────────┘
typ                 └┘  └─┘  └───────────┘    └┘  └────────┘      
doc                                               
609      by refine eq.to_iff (congr_arg S $ funext $ λs, _); {cases s with a b, refl, cases b}
id                 └───────┘  └───────┘    └────┘                                         
src         └─────┘└───────┘ └───────┘  └────┘  └───┘   └────┘ └───────┘  └──┘  └────┘
typ         └─────┘└───────┘ └───────┘ └────┘  └───┘   └────┘└───────┘  └──┘  └────┘
doc         └─────┘                             └───┘   └────┘ └───────┘  └──┘  └────┘
txt         └─────┘                             └───┘   └────┘ └───────┘  └──┘  └────┘
par         └─────┘                             └───┘   └────┘ └───────┘  └──┘  └────┘
pid                                            └───┘         └───────┘             
st         └────────────────────────────────────────────────┘└───────────────┘└────┘└───────┘└┘
610    | (succ n) S d f := f.cons_elim $ λf fl, by simp; exact λ df dfl,
id        └──┘             └────────┘     └┘
src       └──┘              └────────┘             └──┘  └────┘ └────────
typ       └──┘             └────────┘     └┘     └──┘  └────┘ └────────
doc                                                └──┘  └────┘ └────────
txt                                                └──┘  └────┘ └────────
par                                                └──┘  └────┘ └────────
pid                                                            └────────
st                                                └──────────────────────
611      have dioph (λv, S (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr)),
id                                              └┘
src  ───┘    └─────┘  └─┘             └┘└┘     └───
typ  ───┘    └─────┘  └─┘             └┘└┘     └───
doc  ───┘    └─────┘  └─┘              └┘└┘     └───
txt  ───┘    └─────┘  └─┘               └┘       └───
par  ───┘    └─────┘  └─┘               └┘       └───
pid  ───┘    └─────┘  └─┘               └┘       └───
st   ───────────────────────────────────────────────────────────
612      from ext (dioph_fn_comp1 (reindex_dioph d (some ∘ inl ⊗ none :: some ∘ inr)) (reindex_dioph_fn df inl)) $
id            └─┘  └────────────┘  └───────────┘                └──┘    └──┘   └─┘    └──────────────┘    └─┘
src  ────────┘└─┘ └────────────┘ └───────────┘           └──┘  └──┘ └─┘└─┘ └──────────────┘  └─┘└─┘ 
typ  ────────┘└─┘ └────────────┘ └───────────┘          └──┘  └──┘ └─┘└─┘ └──────────────┘  └─┘└─┘ 
doc  ────────┘                                                         └─┘                      └─┘ 
txt  ────────┘                                                         └─┘                      └─┘ 
par  ────────┘                                                         └─┘                      └─┘ 
pid  ────────┘                                                         └─┘                      └─┘ 
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
613        λv, by {refine eq.to_iff (congr_arg S $ funext $ λs, _); cases s with a b, refl, cases b; refl},
id                        └───────┘  └───────┘    └────┘                                        
src  ─────┘ └─┘  └┘└─────┘└───────┘ └───────┘  └────┘  └───┘└┘└────┘ └───────┘└┘└──┘└┘└────┘ └┘└──┘└──
typ  ─────┘ └─┘  └───────┘└───────┘ └───────┘ └────┘  └─────┘└────┘└───────┘└┘└──┘└┘└────┘└┘└──┘└──
doc  ─────┘ └─┘  └┘└─────┘                             └───┘└┘└────┘ └───────┘└┘└──┘└┘└────┘ └┘└──┘└──
txt  ─────┘ └─┘  └┘└─────┘                             └───┘└┘└────┘ └───────┘└┘└──┘└┘└────┘ └┘└──┘└──
par  ─────┘ └─┘  └───────┘                             └─────┘└────┘ └───────┘└┘└──┘└┘└────┘ └┘└──┘└──
pid  ─────┘ └─┘  └───────┘                             └───────────┘ └─────────────────────┘ └────────
st   ───────────┘└─────────────────────────────────────────────────────────────────┘└────┘└─────────────┘└─
614      have dioph (λv, S (v ⊗ f v :: λ (i : fin2 n), fl i v)),
id                                            └──┘     └┘
src  ───┘    └─────┘  └─┘         └────┘└──┘ └─┘    └───
typ  ───┘    └─────┘  └─┘         └────┘└──┘ └─┘└┘  └───
doc  ───┘    └─────┘  └─┘         └────┘└──┘ └─┘    └───
txt  ───┘    └─────┘  └─┘         └────┘     └─┘    └───
par  ───┘    └─────┘  └─┘         └────┘     └─┘    └───
pid  ───┘    └─────┘  └─┘         └────┘     └─┘    └───
st   ────────────────────────────────────────────────────────────
615      from @dioph_fn_compn n (λv, S (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr)) this _ dfl,
id             └────────────┘                   
src  ────────┘                  └─┘               └┘       └─┘    └─┘   └─
typ  ────────┘ └────────────┘  └─┘             └┘       └─┘    └─┘   └─
doc  ────────┘                  └─┘               └┘       └─┘    └─┘   └─
txt  ────────┘                  └─┘               └┘       └─┘    └─┘   └─
par  ────────┘                  └─┘               └┘       └─┘    └─┘   └─
pid  ────────┘                  └─┘               └┘       └─┘    └─┘   └─
st   ──────────────────────────────────────────────────────────────────────────────────
616      ext this $ λv, by rw [
src  ───┘         └─┘  └────
typ  ───┘         └─┘  └────
doc  ───┘         └─┘  └────
txt  ───┘         └─┘  └────
par  ───┘         └─┘  └────
pid  ───┘         └─┘  └─────
st   ────────────────────┘└─────
617        show cons (f v) (λ (i : fin2 n), fl i v) = λ (i : fin2 (succ n)), (f :: fl) i v,
id              └──┘                                        └──┘  └──┘          └┘    
src  ─────┘    └──┘   └┘  └────┘     └─┘    └┘ └────┘└──┘ └──┘ └──┘      └┘  └─
typ  ─────┘    └──┘   └┘  └────┘     └─┘    └┘ └────┘└──┘ └──┘└──┘   └┘└┘ └─
doc  ─────┘    └──┘   └┘  └────┘     └─┘    └┘  └────┘└──┘      └──┘      └┘  └─
txt  ─────┘           └┘  └────┘     └─┘    └┘  └────┘          └──┘      └┘  └─
par  ─────┘           └┘  └────┘     └─┘    └┘  └────┘          └──┘      └┘  └─
pid  ─────┘           └┘  └────┘     └─┘    └┘  └────┘          └──┘      └┘  └─
st   ───────────────────────────────────────────────────────────────────────────────────────
618        from funext $ λs, by cases s with a b; refl]
id              └────┘                
src  ──────────┘└────┘  └─┘  └────┘ └───────┘└┘└──┘└─
typ  ──────────┘└────┘  └─┘  └────┘└───────┘└┘└──┘└─
doc  ──────────┘        └─┘  └────┘ └───────┘└┘└──┘└─
txt  ──────────┘        └─┘  └────┘ └───────┘└┘└──┘└─
par  ──────────┘        └─┘  └────┘ └───────┘└┘└──┘└─
pid  ──────────┘        └─┘  └─────┘ └────────────────
st   ─────────────────────────┘└─────────────────────┘
619  
src  
typ  
doc  
txt  
par  
pid  
st   
620    theorem dioph_comp {n} {S : set (vector3 ℕ n)} (d : dioph S)
id                                 └─┘  └─────┘          └───┘ 
src  ─┘                            └─┘  └─────┘           └───┘
typ  ─┘                            └─┘  └─────┘          └───┘ 
doc  ─┘                                 └─────┘            └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
621      (f : vector3 ((α → ℕ) → ℕ) n) (df : vector_allp dioph_fn f) : dioph (λv, S (λi, f i v)) :=
id            └─────┘                   └─────────┘ └──────┘     └───┘            
src           └─────┘                      └─────────┘ └──────┘      └───┘
typ           └─────┘                   └─────────┘ └──────┘     └───┘            
doc           └─────┘                        └─────────┘ └──────┘      └───┘
622    dioph_fn_compn (reindex_dioph d inr) df
id     └────────────┘  └───────────┘  └─┘  └┘
src    └────────────┘  └───────────┘   └─┘
typ    └────────────┘  └───────────┘  └─┘  └┘
623  
624    theorem dioph_fn_comp {n} {f : vector3 ℕ n → ℕ} (df : dioph_fn f)
id                                    └─────┘             └──────┘ 
src                                   └─────┘              └──────┘
typ                                   └─────┘             └──────┘ 
doc                                   └─────┘                └──────┘
625      (g : vector3 ((α → ℕ) → ℕ) n) (dg : vector_allp dioph_fn g) : dioph_fn (λv, f (λi, g i v)) :=
id            └─────┘                   └─────────┘ └──────┘     └──────┘            
src           └─────┘                      └─────────┘ └──────┘      └──────┘
typ           └─────┘                   └─────────┘ └──────┘     └──────┘            
doc           └─────┘                        └─────────┘ └──────┘      └──────┘
626    dioph_comp ((dioph_fn_vec _).1 df) ((λv, v none) :: λi v, g i (v ∘ some)) $
id     └────────┘   └──────────┘     └┘        └──┘  └┘          └──┘
src    └────────┘   └──────────┘                 └──┘  └┘               └──┘
typ    └────────┘   └──────────┘     └┘        └──┘  └┘          └──┘
doc                                                     └┘
627    by simp; exact ⟨proj_dioph none, (vector_allp_iff_forall _ _).2 $ λi,
id                     └────────┘ └──┘
src       └──┘  └────┘ └────────┘└──┘└┘                       └──────┘  └──
typ       └──┘  └────┘ └────────┘└──┘└┘                       └──────┘  └──
doc       └──┘  └────┘               └┘                       └──────┘  └──
txt       └──┘  └────┘               └┘                       └──────┘  └──
par       └──┘  └────┘               └┘                       └──────┘  └──
pid                                 └┘                       └──────┘  └──
st       └───────────────────────────────────────────────────────────────────
628      reindex_dioph_fn ((vector_allp_iff_forall _ _).1 dg _) _⟩
id       └──────────────┘   └────────────────────┘        └┘
src  ───┘└──────────────┘  └────────────────────┘└──────┘  └──────
typ  ───┘└──────────────┘  └────────────────────┘└──────┘└┘└──────
doc  ───┘                                        └──────┘  └──────
txt  ───┘                                        └──────┘  └──────
par  ───┘                                        └──────┘  └──────
pid  ───┘                                        └──────┘  └────┘
st   ──────────────────────────────────────────────────────────────
629  
src  
typ  
doc  
txt  
par  
pid  
st   
630    localized "notation x ` D∧ `:35 y := dioph.and_dioph x y" in dioph
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
631    localized "notation x ` D∨ `:35 y := dioph.or_dioph x y" in dioph
632  
633    localized "notation `D∃`:30 := dioph.vec_ex1_dioph" in dioph
634  
635    localized "prefix `&`:max := of_nat'" in dioph
636    theorem proj_dioph_of_nat {n : ℕ} (m : ℕ) [is_lt m n] : dioph_fn (λv : vector3 ℕ n, v &m) :=
id                                              └───┘      └──────┘       └─────┘     
src                                             └───┘        └──────┘       └─────┘       
typ                                             └───┘      └──────┘       └─────┘     
doc                                               └───┘        └──────┘       └─────┘        
637    proj_dioph &m
id     └────────┘ 
src    └────────┘ 
typ    └────────┘ 
doc               
638    localized "prefix `D&`:100 := dioph.proj_dioph_of_nat" in dioph
639  
640    theorem const_dioph (n : ℕ) : dioph_fn (const (α → ℕ) n) :=
id                                  └──────┘  └───┘       
src                                 └──────┘  └───┘      
typ                                 └──────┘  └───┘       
doc                                  └──────┘
641    abs_poly_dioph (poly.const n)
id     └────────────┘  └────────┘ 
src    └────────────┘  └────────┘
typ    └────────────┘  └────────┘ 
doc                    └────────┘
642    localized "prefix `D.`:100 := dioph.const_dioph" in dioph
643  
644    variables {f g : (α → ℕ) → ℕ} (df : dioph_fn f) (dg : dioph_fn g)
id                                      └──────┘          └──────┘
src                                      └──────┘          └──────┘
typ                                     └──────┘          └──────┘
doc                                        └──────┘          └──────┘
645    include df dg
646  
647    theorem dioph_comp2 {S : ℕ → ℕ → Prop} (d : dioph (λv:vector3 ℕ 2, S (v &0) (v &1))) :
id                                               └───┘     └─────┘             
src                                              └───┘     └─────┘                
typ                                              └───┘     └─────┘             
doc                                                └───┘     └─────┘                 
648      dioph (λv, S (f v) (g v)) :=
id       └───┘            
src      └───┘
typ      └───┘            
doc      └───┘
649    dioph_comp d [f, g] (by exact ⟨df, dg⟩)
id     └────────┘               └┘  └┘
src    └────────┘           └────┘   └┘  
typ    └────────┘        └────┘ └┘└┘└┘
doc                         └────┘   └┘  
txt                            └────┘   └┘  
par                            └────┘   └┘  
pid                                    └┘  
st                            └─────────────┘
650  
651    theorem dioph_fn_comp2 {h : ℕ → ℕ → ℕ} (d : dioph_fn (λv:vector3 ℕ 2, h (v &0) (v &1))) :
id                                              └──────┘     └─────┘             
src                                             └──────┘     └─────┘                
typ                                             └──────┘     └─────┘             
doc                                                └──────┘     └─────┘                 
652      dioph_fn (λv, h (f v) (g v)) :=
id       └──────┘            
src      └──────┘
typ      └──────┘            
doc      └──────┘
653    dioph_fn_comp d [f, g] (by exact ⟨df, dg⟩)
id     └───────────┘               └┘  └┘
src    └───────────┘           └────┘   └┘  
typ    └───────────┘        └────┘ └┘└┘└┘
doc                            └────┘   └┘  
txt                               └────┘   └┘  
par                               └────┘   └┘  
pid                                       └┘  
st                               └─────────────┘
654  
655    theorem eq_dioph : dioph (λv, f v = g v) :=
id                        └───┘         
src                       └───┘          
typ                       └───┘         
doc                       └───┘
656    dioph_comp2 df dg $ of_no_dummies _ (poly.proj &0 - poly.proj &1)
id     └─────────┘ └┘ └┘   └───────────┘    └───────┘    └───────┘ 
src    └─────────┘         └───────────┘    └───────┘    └───────┘ 
typ    └─────────┘ └┘ └┘   └───────────┘    └───────┘    └───────┘ 
doc                                         └───────┘     └───────┘ 
657      (λv, (int.coe_nat_eq_coe_nat_iff _ _).symm.trans
id            └────────────────────────┘     └──┘ └───┘
src            └────────────────────────┘     └──┘ └───┘
typ           └────────────────────────┘     └──┘ └───┘
658      ⟨@sub_eq_zero_of_eq ℤ _ (v &0) (v &1), eq_of_sub_eq_zero⟩)
id         └───────────────┘               └───────────────┘
src        └───────────────┘                 └───────────────┘
typ        └───────────────┘               └───────────────┘
doc                                       
659    localized "infix ` D= `:50 := dioph.eq_dioph" in dioph
660  
661    theorem add_dioph : dioph_fn (λv, f v + g v) :=
id                         └──────┘         
src                        └──────┘          
typ                        └──────┘         
doc                        └──────┘
662    dioph_fn_comp2 df dg $ abs_poly_dioph (poly.proj &0 + poly.proj &1)
id     └────────────┘ └┘ └┘   └────────────┘  └───────┘    └───────┘ 
src    └────────────┘         └────────────┘  └───────┘    └───────┘ 
typ    └────────────┘ └┘ └┘   └────────────┘  └───────┘    └───────┘ 
doc                                           └───────┘     └───────┘ 
663    localized "infix ` D+ `:80 := dioph.add_dioph" in dioph
664  
665    theorem mul_dioph : dioph_fn (λv, f v * g v) :=
id                         └──────┘         
src                        └──────┘          
typ                        └──────┘         
doc                        └──────┘
666    dioph_fn_comp2 df dg $ abs_poly_dioph (poly.proj &0 * poly.proj &1)
id     └────────────┘ └┘ └┘   └────────────┘  └───────┘    └───────┘ 
src    └────────────┘         └────────────┘  └───────┘    └───────┘ 
typ    └────────────┘ └┘ └┘   └────────────┘  └───────┘    └───────┘ 
doc                                           └───────┘     └───────┘ 
667    localized "infix ` D* `:90 := dioph.mul_dioph" in dioph
668  
669    theorem le_dioph : dioph (λv, f v ≤ g v) :=
id                        └───┘         
src                       └───┘          
typ                       └───┘         
doc                       └───┘
670    dioph_comp2 df dg $ ext (D∃2 $ D&1 D+ D&0 D= D&2) (λv, ⟨λ⟨x, hx⟩, le.intro hx, le.dest⟩)
id     └─────────┘ └┘ └┘   └─┘  └┘    └┘  └┘ └┘  └┘ └┘            └┘   └──────┘     └─────┘
src    └─────────┘         └─┘  └┘    └┘  └┘ └┘  └┘ └┘                   └──────┘     └─────┘
typ    └─────────┘ └┘ └┘   └─┘  └┘    └┘  └┘ └┘  └┘ └┘            └┘   └──────┘     └─────┘
671    localized "infix ` D≤ `:50 := dioph.le_dioph" in dioph
672  
673    theorem lt_dioph : dioph (λv, f v < g v) := df D+ (D. 1) D≤ dg
id                        └───┘              └┘ └┘  └┘     └┘ └┘
src                       └───┘                      └┘  └┘     └┘
typ                       └───┘              └┘ └┘  └┘     └┘ └┘
doc                       └───┘
674    localized "infix ` D< `:50 := dioph.lt_dioph" in dioph
675  
676    theorem ne_dioph : dioph (λv, f v ≠ g v) :=
id                        └───┘         
src                       └───┘          
typ                       └───┘         
doc                       └───┘
677    ext (df D< dg D∨ dg D< df) $ λv, ne_iff_lt_or_gt.symm
id     └─┘  └┘ └┘ └┘ └┘ └┘ └┘ └┘       └─────────────┘└───┘
src    └─┘     └┘    └┘    └┘           └─────────────┘└───┘
typ    └─┘  └┘ └┘ └┘ └┘ └┘ └┘ └┘       └─────────────┘└───┘
678    localized "infix ` D≠ `:50 := dioph.ne_dioph" in dioph
679  
680    theorem sub_dioph : dioph_fn (λv, f v - g v) :=
id                         └──────┘         
src                        └──────┘          
typ                        └──────┘         
doc                        └──────┘
681    dioph_fn_comp2 df dg $ (dioph_fn_vec _).2 $
id     └────────────┘ └┘ └┘    └──────────┘   
src    └────────────┘          └──────────┘   
typ    └────────────┘ └┘ └┘    └──────────┘   
682    ext (D&1 D= D&0 D+ D&2 D∨ D&1 D≤ D&2 D∧ D&0 D= D.0) $ (vector_all_iff_forall _).1 $ λx y z,
id     └─┘  └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘       └───────────────────┘          
src    └─┘  └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘       └───────────────────┘   
typ    └─┘  └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘       └───────────────────┘          
683    show (y = x + z ∨ y ≤ z ∧ x = 0) ↔ y - z = x, from
id                               
src                                     
typ                              
684    ⟨λo, begin
id       
typ      
st          └─────
685      rcases o with ae | ⟨yz, x0⟩,
id              
src      └─────┘ └─────────────────┘
typ      └─────┘└─────────────────┘
doc      └─────┘ └─────────────────┘
txt      └─────┘ └─────────────────┘
par      └─────┘ └─────────────────┘
pid             └─────────────────┘
st   ──────────────────────────────┘└─
686      { rw [ae, nat.add_sub_cancel] },
id             └┘  └────────────────┘
src        └──┘  └┘└────────────────┘└┘
typ        └──┘└┘└┘└────────────────┘└┘
doc        └──┘  └┘                  └┘
txt        └──┘  └┘                  └┘
par        └──┘  └┘                  └┘
pid          └┘  └┘                  
st   ─────┘└────┘└──────────────────┘└┘
687      { rw [x0, nat.sub_eq_zero_of_le yz] }
id             └┘  └───────────────────┘ └┘
src        └──┘  └┘└───────────────────┘  └┘
typ        └──┘└┘└┘└───────────────────┘└┘└┘
doc        └──┘  └┘                       └┘
txt        └──┘  └┘                       └┘
par        └──┘  └┘                       └┘
pid          └┘  └┘                       
st   ───────────┘└────────────────────────┘└─
688    end, λh, begin
id           
typ          
st   ────┘      └─────
689      subst x,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────┘└─
690      cases le_total y z with yz zy,
id             └──────┘  
src      └────┘└──────┘  └─────────┘
typ      └────┘└──────┘└─────────┘
doc      └────┘          └─────────┘
txt      └────┘          └─────────┘
par      └────┘          └─────────┘
pid                     └─────────┘
st   ────────────────────────────────┘└─
691      { exact or.inr ⟨yz, nat.sub_eq_zero_of_le yz⟩ },
id               └────┘      └───────────────────┘ └┘
src        └────┘└────┘   └┘└───────────────────┘  └┘
typ        └────┘└────┘   └┘└───────────────────┘└┘└┘
doc        └────┘         └┘                       └┘
txt        └────┘         └┘                       └┘
par        └────┘         └┘                       └┘
pid                      └┘                       
st   ─────┘└──────────────────────────────────────────┘└┘
692      { exact or.inl (nat.sub_add_cancel zy).symm },
id               └────┘  └────────────────┘ └┘
src        └────┘└────┘ └────────────────┘  └─────┘
typ        └────┘└────┘ └────────────────┘└┘└─────┘
doc        └────┘                           └─────┘
txt        └────┘                           └─────┘
par        └────┘                           └─────┘
pid                                        └───┘└┘
st   ───────────────────────────────────────────────┘└──
693    end⟩
st   ────┘
694    localized "infix ` D- `:80 := dioph.sub_dioph" in dioph
695  
696    theorem dvd_dioph : dioph (λv, f v ∣ g v) :=
id                         └───┘         
src                        └───┘          
typ                        └───┘         
doc                        └───┘
697    dioph_comp (D∃2 $ D&2 D= D&1 D* D&0) [f, g] (by exact ⟨df, dg⟩)
id     └────────┘  └┘    └┘  └┘ └┘  └┘ └┘                └┘  └┘
src    └────────┘  └┘    └┘  └┘ └┘  └┘ └┘           └────┘   └┘  
typ    └────────┘  └┘    └┘  └┘ └┘  └┘ └┘         └────┘ └┘└┘└┘
doc                                                 └────┘   └┘  
txt                                                    └────┘   └┘  
par                                                    └────┘   └┘  
pid                                                            └┘  
st                                                    └─────────────┘
698    localized "infix ` D∣ `:50 := dioph.dvd_dioph" in dioph
699  
700    theorem mod_dioph : dioph_fn (λv, f v % g v) :=
id                         └──────┘         
src                        └──────┘          
typ                        └──────┘         
doc                        └──────┘
701    have dioph (λv : vector3 ℕ 3, (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ (x : ℕ), v &0 + v &2 * x = v &1),
id          └───┘       └─────┘                                         
src         └───┘       └─────┘                                                
typ         └───┘       └─────┘                                         
doc         └───┘       └─────┘                                                           
702    from (D&2 D= D.0 D∨ D&0 D< D&2) D∧ (D∃3 $ D&1 D+ D&3 D* D&0 D= D&2),
id           └┘  └┘ └┘   └┘ └┘  └┘ └┘   └┘  └┘    └┘  └┘ └┘  └┘ └┘  └┘ └┘
src          └┘  └┘ └┘   └┘ └┘  └┘ └┘   └┘  └┘    └┘  └┘ └┘  └┘ └┘  └┘ └┘
typ          └┘  └┘ └┘   └┘ └┘  └┘ └┘   └┘  └┘    └┘  └┘ └┘  └┘ └┘  └┘ └┘
703    dioph_fn_comp2 df dg $ (dioph_fn_vec _).2 $ ext this $ (vector_all_iff_forall _).1 $ λz x y,
id     └────────────┘ └┘ └┘    └──────────┘       └─┘ └──┘    └───────────────────┘          
src    └────────────┘          └──────────┘       └─┘         └───────────────────┘   
typ    └────────────┘ └┘ └┘    └──────────┘       └─┘ └──┘    └───────────────────┘          
704    show ((y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x) ↔ x % y = z, from
id                                     
src                                             
typ                                    
705    ⟨λ⟨h, c, hc⟩, begin rw ← hc; simp; cases h with x0 hl, rw [x0, mod_zero], exact mod_eq_of_lt hl end,
id                             └┘                               └┘  └──────┘         └──────────┘ └┘
src                        └───┘    └──┘  └────┘ └─────────┘  └──┘  └┘└──────┘  └────┘└──────────┘  
typ                       └───┘└┘  └──┘  └────┘└─────────┘  └──┘└┘└┘└──────┘  └────┘└──────────┘└┘
doc                        └───┘    └──┘  └────┘ └─────────┘  └──┘  └┘          └────┘              
txt                        └───┘    └──┘  └────┘ └─────────┘  └──┘  └┘          └────┘              
par                        └───┘    └──┘  └────┘ └─────────┘  └──┘  └┘          └────┘              
pid                          └─┘                └─────────┘    └┘  └┘                             
st                   └─────────────────────────────────────┘└────┘└┘└────────┘└──────────────────────┘└─┘
706    λe, by rw ← e; exact ⟨or_iff_not_imp_left.2 $ λh, mod_lt _ (nat.pos_of_ne_zero h), x / y, mod_add_div _ _⟩⟩
id                         └─────────────────┘         └────┘    └────────────────┘         └─────────┘
src           └───┘   └────┘ └─────────────────┘└─┘  └─┘└────┘└─┘ └────────────────┘ └─┘  └┘└─────────┘└───┘
typ          └───┘  └────┘ └─────────────────┘└─┘  └─┘└────┘└─┘ └────────────────┘ └─┘└┘└─────────┘└───┘
doc           └───┘   └────┘                    └─┘  └─┘      └─┘                    └─┘   └┘           └───┘
txt           └───┘   └────┘                    └─┘  └─┘      └─┘                    └─┘   └┘           └───┘
par           └───┘   └────┘                    └─┘  └─┘      └─┘                    └─┘   └┘           └───┘
pid             └─┘                            └─┘  └─┘      └─┘                    └─┘   └┘           └───┘
st           └──────────────────────────────────────────────────────────────────────────────────────────────────┘
707    localized "infix ` D% `:80 := dioph.mod_dioph" in dioph
708  
709    theorem modeq_dioph {h : (α → ℕ) → ℕ} (dh : dioph_fn h) : dioph (λv, f v ≡ g v [MOD h v]) :=
id                                             └──────┘     └───┘          └──┘  
src                                              └──────┘      └───┘               └──┘    
typ                                            └──────┘     └───┘          └──┘  
doc                                                └──────┘      └───┘               └──┘    
710    df D% dh D= dg D% dh
id     └┘ └┘ └┘ └┘ └┘ └┘ └┘
src       └┘    └┘    └┘
typ    └┘ └┘ └┘ └┘ └┘ └┘ └┘
711    localized "notation `D≡` := dioph.modeq_dioph" in dioph
712  
713    theorem div_dioph : dioph_fn (λv, f v / g v) :=
id                         └──────┘         
src                        └──────┘          
typ                        └──────┘         
doc                        └──────┘
714    have dioph (λv : vector3 ℕ 3, v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2),
id          └───┘       └─────┘                                             
src         └───┘       └─────┘                                                     
typ         └───┘       └─────┘                                             
doc         └───┘       └─────┘                                                                
715    from (D&2 D= D.0 D∧ D&0 D= D.0) D∨ D&0 D* D&2 D≤ D&1 D∧ D&1 D< (D&0 D+ D.1) D* D&2,
id           └┘  └┘ └┘   └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘  └┘  └┘ └┘    └┘ └┘
src          └┘  └┘ └┘   └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘  └┘  └┘ └┘    └┘ └┘
typ          └┘  └┘ └┘   └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘  └┘  └┘ └┘    └┘ └┘
716    dioph_fn_comp2 df dg $ (dioph_fn_vec _).2 $ ext this $ (vector_all_iff_forall _).1 $ λz x y,
id     └────────────┘ └┘ └┘    └──────────┘       └─┘ └──┘    └───────────────────┘          
src    └────────────┘          └──────────┘       └─┘         └───────────────────┘   
typ    └────────────┘ └┘ └┘    └──────────┘       └─┘ └──┘    └───────────────────┘          
717    show y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z,
id                                         
src                                                 
typ                                        
718    by refine iff.trans _ eq_comm; exact y.eq_zero_or_pos.elim
id               └───────┘   └─────┘        └───────────────────┘
src       └─────┘└───────┘└─┘└─────┘  └────┘└───────────────────┘
typ       └─────┘└───────┘└─┘└─────┘  └────┘└───────────────────┘
doc       └─────┘         └─┘         └────┘                     
txt       └─────┘         └─┘         └────┘                     
par       └─────┘         └─┘         └────┘                     
pid                      └─┘                                   
st       └────────────────────────────────────────────────────────
719      (λy0, by rw [y0, nat.div_zero]; exact
id                    └┘  └──────────┘
src  ───┘  └──┘  └──┘  └┘└──────────┘└───────
typ  ───┘  └──┘  └──┘└┘└┘└──────────┘└───────
doc  ───┘  └──┘  └──┘  └┘            └───────
txt  ───┘  └──┘  └──┘  └┘            └───────
par  ───┘  └──┘  └──┘  └┘            └───────
pid  ───┘  └──┘  └───┘  └┘            └────────
st   ───────────┘└─────┘└────────────┘└───────
720        ⟨λo, (o.resolve_right $ λ⟨_, h2⟩, not_lt_zero _ h2).right, λz0, or.inl ⟨rfl, z0⟩⟩)
id                └────────────┘        └┘   └─────────┘                   └────┘  └─┘
src  ─────┘  └─┘  └────────────┘  └──┘  └─┘└─────────┘└─┘  └───────┘ └──┘└────┘ └─┘└┘  └───
typ  ─────┘  └─┘  └────────────┘  └──┘└┘└─┘└─────────┘└─┘  └───────┘ └──┘└────┘ └─┘└┘  └───
doc  ─────┘  └─┘                  └──┘  └─┘           └─┘  └───────┘ └──┘          └┘  └───
txt  ─────┘  └─┘                  └──┘  └─┘           └─┘  └───────┘ └──┘          └┘  └───
par  ─────┘  └─┘                  └──┘  └─┘           └─┘  └───────┘ └──┘          └┘  └───
pid  ─────┘  └─┘                  └──┘  └─┘           └─┘  └───────┘ └──┘          └┘  └───
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
721      (λypos, iff.trans ⟨λo, o.resolve_left $ λ⟨h1, _⟩, ne_of_gt ypos h1, or.inr⟩
id                               └───────────┘     └┘      └──────┘          └────┘
src  ───┘  └────┘           └─┘ └───────────┘    └────┘└──────┘      └┘└────┘└─
typ  ───┘  └────┘           └─┘ └───────────┘  └┘└────┘└──────┘      └┘└────┘└─
doc  ───┘  └────┘           └─┘                  └────┘              └┘      └─
txt  ───┘  └────┘           └─┘                  └────┘              └┘      └─
par  ───┘  └────┘           └─┘                  └────┘              └┘      └─
pid  ───┘  └────┘           └─┘                  └────┘              └┘      └─
st   ────────────────────────────────────────────────────────────────────────────────
722        (le_antisymm_iff.trans $ and_congr (nat.le_div_iff_mul_le _ _ ypos) $
id          └───────────────────┘   └───────┘  └───────────────────┘
src  ─────┘ └───────────────────┘ └───────┘ └───────────────────┘└───┘    └┘ 
typ  ─────┘ └───────────────────┘ └───────┘ └───────────────────┘└───┘    └┘ 
doc  ─────┘                                                      └───┘    └┘ 
txt  ─────┘                                                      └───┘    └┘ 
par  ─────┘                                                      └───┘    └┘ 
pid  ─────┘                                                      └───┘    └┘ 
st   ────────────────────────────────────────────────────────────────────────────
723          iff.trans ⟨lt_succ_of_le, le_of_lt_succ⟩ (div_lt_iff_lt_mul _ _ ypos)).symm)
id           └───────┘  └───────────┘  └───────────┘   └───────────────┘
src  ───────┘└───────┘ └───────────┘└┘└───────────┘└┘ └───────────────┘└───┘    └────────
typ  ───────┘└───────┘ └───────────┘└┘└───────────┘└┘ └───────────────┘└───┘    └────────
doc  ───────┘                       └┘             └┘                  └───┘    └────────
txt  ───────┘                       └┘             └┘                  └───┘    └────────
par  ───────┘                       └┘             └┘                  └───┘    └────────
pid  ───────┘                       └┘             └┘                  └───┘    └──────┘
st   ─────────────────────────────────────────────────────────────────────────────────────
724    localized "infix ` D/ `:80 := dioph.div_dioph" in dioph
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
725  
726    omit df dg
727    open pell
728  
729    theorem pell_dioph : dioph (λv:vector3 ℕ 4, ∃ h : v &0 > 1,
id                          └───┘     └─────┘               
src                         └───┘     └─────┘                
typ                         └───┘     └─────┘               
doc                         └───┘     └─────┘              
730      xn h (v &1) = v &2 ∧ yn h (v &1) = v &3) :=
id       └┘            └┘         
src      └┘               └┘            
typ      └┘            └┘         
doc      └┘                 └┘             
731    have dioph {v : vector3 ℕ 4 |
id          └───┘     └─────┘ 
src         └───┘     └─────┘ 
typ         └───┘     └─────┘ 
doc         └───┘      └─────┘
732    v &0 > 1 ∧ v &1 ≤ v &3 ∧
id                   
src                     
typ                  
doc                      
733    (v &2 = 1 ∧ v &3 = 0 ∨
id                   
src                    
typ                  
doc                 
734    ∃ (u w s t b : ℕ),
id                    
src                   
typ                   
735      v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
id                                      
src                                           
typ                                     
doc                                            
736      u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
id                              
src                                   
typ                             
doc                       
737      s * s - (b * b - 1) * t * t = 1 ∧
id                          
src                               
typ                         
738      b > 1 ∧ (b ≡ 1 [MOD 4 * v &3]) ∧ (b ≡ v &0 [MOD u]) ∧
id                 └──┘               └──┘   
src                  └──┘                  └──┘    
typ                └──┘               └──┘   
doc                    └──┘                    └──┘  
739      w > 0 ∧ v &3 * v &3 ∣ w ∧
id                     
src                        
typ                    
doc                      
740      (s ≡ v &2 [MOD u]) ∧
id             └──┘   
src              └──┘    
typ            └──┘   
doc              └──┘  
741      (t ≡ v &1 [MOD 4 * v &3]))}, from
id             └──┘      
src              └──┘       
typ            └──┘      
doc              └──┘        
742    D.1 D< D&0 D∧ D&1 D≤ D&3 D∧
id     └┘   └┘ └┘  └┘ └┘  └┘ └┘  └┘
src    └┘   └┘ └┘  └┘ └┘  └┘ └┘  └┘
typ    └┘   └┘ └┘  └┘ └┘  └┘ └┘  └┘
743    ((D&2 D= D.1 D∧ D&3 D= D.0) D∨
id       └┘  └┘ └┘   └┘ └┘  └┘ └┘    
src      └┘  └┘ └┘   └┘ └┘  └┘ └┘    
typ      └┘  └┘ └┘   └┘ └┘  └┘ └┘    
744     (D∃4 $ D∃5 $ D∃6 $ D∃7 $ D∃8 $
id       └┘    └┘    └┘    └┘    └┘
src      └┘    └┘    └┘    └┘    └┘
typ      └┘    └┘    └┘    └┘    └┘
745      D&7 D* D&7 D- (D&5 D* D&5 D- D.1) D* D&8 D* D&8 D= D.1 D∧
id       └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘   
src      └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘   
typ      └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘   
746      D&4 D* D&4 D- (D&5 D* D&5 D- D.1) D* D&3 D* D&3 D= D.1 D∧
id       └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘   
src      └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘   
typ      └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘   
747      D&2 D* D&2 D- (D&0 D* D&0 D- D.1) D* D&1 D* D&1 D= D.1 D∧
id       └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘   
src      └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘   
typ      └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    └┘ └┘  └┘ └┘  └┘ └┘   
748      D.1 D< D&0 D∧ (D≡ (D&0) (D.1) (D.4 D* D&8)) D∧ (D≡ (D&0) (D&5) D&4) D∧
id       └┘   └┘ └┘  └┘  └┘  └┘    └┘     └┘   └┘ └┘    └┘  └┘  └┘    └┘   └┘
src      └┘   └┘ └┘  └┘  └┘  └┘    └┘     └┘   └┘ └┘    └┘  └┘  └┘    └┘   └┘
typ      └┘   └┘ └┘  └┘  └┘  └┘    └┘     └┘   └┘ └┘    └┘  └┘  └┘    └┘   └┘
749      D.0 D< D&3 D∧ D&8 D* D&8 D∣ D&3 D∧
id       └┘   └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘
src      └┘   └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘
typ      └┘   └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘
750      (D≡ (D&2) (D&7) D&4) D∧
id        └┘  └┘    └┘   └┘   └┘
src       └┘  └┘    └┘   └┘   └┘
typ       └┘  └┘    └┘   └┘   └┘
751      (D≡ (D&1) (D&6) (D.4 D* D&8)))),
id        └┘  └┘    └┘    └┘   └┘ └┘
src       └┘  └┘    └┘    └┘   └┘ └┘
typ       └┘  └┘    └┘    └┘   └┘ └┘
752    dioph.ext this $ λv, matiyasevic.symm
id     └───────┘ └──┘      └─────────┘└───┘
src    └───────┘            └─────────┘└───┘
typ    └───────┘ └──┘      └─────────┘└───┘
753  
754    theorem xn_dioph : dioph_pfun (λv:vector3 ℕ 2, ⟨v &0 > 1, λh, xn h (v &1)⟩) :=
id                        └────────┘     └─────┘                └┘    
src                       └────────┘     └─────┘                  └┘      
typ                       └────────┘     └─────┘                └┘    
doc                       └────────┘     └─────┘                    └┘      
755    have dioph (λv:vector3 ℕ 3, ∃ y, ∃ h : v &1 > 1, xn h (v &2) = v &0 ∧ yn h (v &2) = y), from
id          └───┘     └─────┘                  └┘            └┘        
src         └───┘     └─────┘                    └┘               └┘         
typ         └───┘     └─────┘                  └┘            └┘        
doc         └───┘     └─────┘                          └┘                 └┘      
756    let D_pell := @reindex_dioph _ (fin2 4) _ pell_dioph [&2, &3, &1, &0] in D∃3 D_pell,
id         └────┘     └───────────┘    └──┘      └────────┘            └┘  └────┘
src                   └───────────┘    └──┘      └────────┘            └┘
typ        └────┘     └───────────┘    └──┘      └────────┘            └┘  └────┘
doc                                    └──┘                        
757    (dioph_pfun_vec _).2 $ dioph.ext this $ λv, ⟨λ⟨y, h, xe, ye⟩, ⟨h, xe⟩, λ⟨h, xe⟩, ⟨_, h, xe, rfl⟩⟩
id      └────────────┘       └───────┘ └──┘             └┘                   └┘              └─┘
src     └────────────┘       └───────┘                                                            └─┘
typ     └────────────┘       └───────┘ └──┘             └┘                   └┘              └─┘
758  
759    include df dg
760    theorem pow_dioph : dioph_fn (λv, f v ^ g v) :=
id                         └──────┘         
src                        └──────┘          
typ                        └──────┘         
doc                        └──────┘
761    have dioph {v : vector3 ℕ 3 |
id          └───┘     └─────┘ 
src         └───┘     └─────┘ 
typ         └───┘     └─────┘ 
doc         └───┘      └─────┘
762    v &2 = 0 ∧ v &0 = 1 ∨ v &2 > 0 ∧
id                         
src                           
typ                        
doc                          
763    (v &1 = 0 ∧ v &0 = 0 ∨ v &1 > 0 ∧
id                          
src                            
typ                         
doc                           
764    ∃ (w a t z x y : ℕ),
id                      
src                     
typ                     
765      (∃ (a1 : a > 1), xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
id                    └┘ └┘         └┘ └┘         
src                    └┘              └┘              
typ                   └┘ └┘         └┘ └┘         
doc                       └┘                └┘       
766      (x ≡ y * (a - v &1) + v &0 [MOD t]) ∧
id                       └──┘   
src                           └──┘    
typ                      └──┘   
doc                              └──┘  
767      2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
id                              
src                                  
typ                             
doc                                 
768      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧
id                        
src                             
typ                       
doc                            
769      a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)}, from
id                                         
src                                                
typ                                        
770    let D_pell := @reindex_dioph _ (fin2 9) _ pell_dioph [&4, &8, &1, &0] in
id         └────┘     └───────────┘    └──┘      └────────┘        
src                   └───────────┘    └──┘      └────────┘        
typ        └────┘     └───────────┘    └──┘      └────────┘        
doc                                    └──┘                        
771    (D&2 D= D.0 D∧ D&0 D= D.1) D∨ (D.0 D< D&2 D∧
id      └┘  └┘ └┘   └┘ └┘  └┘ └┘    └┘  └┘   └┘ └┘
src     └┘  └┘ └┘   └┘ └┘  └┘ └┘    └┘  └┘   └┘ └┘
typ     └┘  └┘ └┘   └┘ └┘  └┘ └┘    └┘  └┘   └┘ └┘
772    ((D&1 D= D.0 D∧ D&0 D= D.0) D∨ (D.0 D< D&1 D∧
id       └┘  └┘ └┘   └┘ └┘  └┘ └┘    └┘  └┘   └┘ └┘
src      └┘  └┘ └┘   └┘ └┘  └┘ └┘    └┘  └┘   └┘ └┘
typ      └┘  └┘ └┘   └┘ └┘  └┘ └┘    └┘  └┘   └┘ └┘
773     (D∃3 $ D∃4 $ D∃5 $ D∃6 $ D∃7 $ D∃8 $ D_pell D∧
id       └┘    └┘    └┘    └┘    └┘    └┘    └────┘ └┘
src      └┘    └┘    └┘    └┘    └┘    └┘           └┘
typ      └┘    └┘    └┘    └┘    └┘    └┘    └────┘ └┘
774      (D≡ (D&1) (D&0 D* (D&4 D- D&7) D+ D&6) (D&3)) D∧
id        └┘  └┘    └┘  └┘  └┘  └┘ └┘   └┘ └┘    └┘    └┘
src       └┘  └┘    └┘  └┘  └┘  └┘ └┘   └┘ └┘    └┘    └┘
typ       └┘  └┘    └┘  └┘  └┘  └┘ └┘   └┘ └┘    └┘    └┘
775      D.2 D* D&4 D* D&7 D= D&3 D+ (D&7 D* D&7 D+ D.1) D∧
id       └┘   └┘ └┘  └┘ └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    
src      └┘   └┘ └┘  └┘ └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    
typ      └┘   └┘ └┘  └┘ └┘  └┘ └┘  └┘  └┘  └┘ └┘  └┘ └┘    
776      D&6 D< D&3 D∧ D&7 D≤ D&5 D∧ D&8 D≤ D&5 D∧
id       └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘
src      └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘
typ      └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘ └┘  └┘
777      D&4 D* D&4 D- ((D&5 D+ D.1) D* (D&5 D+ D.1) D- D.1) D* (D&5 D* D&2) D* (D&5 D* D&2) D= D.1)))),
id       └┘  └┘ └┘  └┘   └┘  └┘ └┘    └┘  └┘  └┘ └┘    └┘ └┘    └┘  └┘  └┘ └┘   └┘  └┘  └┘ └┘   └┘ └┘
src      └┘  └┘ └┘  └┘   └┘  └┘ └┘    └┘  └┘  └┘ └┘    └┘ └┘    └┘  └┘  └┘ └┘   └┘  └┘  └┘ └┘   └┘ └┘
typ      └┘  └┘ └┘  └┘   └┘  └┘ └┘    └┘  └┘  └┘ └┘    └┘ └┘    └┘  └┘  └┘ └┘   └┘  └┘  └┘ └┘   └┘ └┘
778    dioph_fn_comp2 df dg $ (dioph_fn_vec _).2 $ dioph.ext this $ λv, iff.symm $
id     └────────────┘ └┘ └┘    └──────────┘       └───────┘ └──┘      └──────┘
src    └────────────┘          └──────────┘       └───────┘            └──────┘
typ    └────────────┘ └┘ └┘    └──────────┘       └───────┘ └──┘      └──────┘
779    eq_pow_of_pell.trans $ or_congr iff.rfl $ and_congr iff.rfl $ or_congr iff.rfl $ and_congr iff.rfl $
id     └────────────┘└────┘   └──────┘ └─────┘   └───────┘ └─────┘   └──────┘ └─────┘   └───────┘ └─────┘
src    └────────────┘└────┘   └──────┘ └─────┘   └───────┘ └─────┘   └──────┘ └─────┘   └───────┘ └─────┘
typ    └────────────┘└────┘   └──────┘ └─────┘   └───────┘ └─────┘   └──────┘ └─────┘   └───────┘ └─────┘
780    ⟨λ⟨w, a, t, z, a1, h⟩, ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩,
id               └┘                             └─┘  └─┘
src                                                   └─┘  └─┘
typ              └┘                             └─┘  └─┘
781     λ⟨w, a, t, z, ._, ._, ⟨a1, rfl, rfl⟩, h⟩, ⟨w, a, t, z, a1, h⟩⟩
id                        └┘       └─┘   
src                                     └─┘
typ                       └┘       └─┘   
782  
783  end
784  end dioph